`BookProof.NavierStokesFlow.Carleman.wron_eq_sum` (c w : ℕ → ℂ) (z : ℂ) (hrec : ∀ n, tridiagFun c w n = z * w n) (N : ℕ) : wron c w N = (z - starRingEnd ℂ z) * ∑ n ∈ Finset.range (

Initializing...

`BookProof.NavierStokesFlow.Carleman.wron_eq_sum` (c w : ℕ → ℂ) (z : ℂ) (hrec : ∀ n, tridiagFun c w n = z * w n) (N : ℕ) : wron c w N = (z - starRingEnd ℂ z) * ∑ n ∈ Finset.range ( · Prove2Me