simp [h]
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
no goals