Theorem: order_pos_iff (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ 0 < FormalMultilinearSeries.order p ↔ ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ 0
Tactic:
simp [pos_iff_ne_zero, (order_eq_zero_iff hp hz₀).not]
State after:
no goals