`BookProof.NavierStokesFlow.LagrangianNS.cauchy_existsUnique` (psi : Fin n → ℂ) : ∃! y : ℝ → Fin n → ℂ, y 0 = psi ∧ ∀ t, HasDerivAt y ((Complex.I • L.hFull) *ᵥ y t) t

Initializing...

`BookProof.NavierStokesFlow.LagrangianNS.cauchy_existsUnique` (psi : Fin n → ℂ) : ∃! y : ℝ → Fin n → ℂ, y 0 = psi ∧ ∀ t, HasDerivAt y ((Complex.I • L.hFull) *ᵥ y t) t · Prove2Me