English
Iterating the dslope/fslope formation preserves the power-series structure of f, replacing p by fslope iterates and dslope by swap iterations.
Русский
Повторение образующих dslope/fslope сохраняет структуру степенной серии; заменяем p на итерации fslope и dslope на повторения swap.
LaTeX
$$$HasFPowerSeriesAt f p z_0 \Rightarrow HasFPowerSeriesAt ((swap dslope z_0)^{[n]} f) (fslope^{[n]} p) z_0$$$
Lean4
/-- The *principle of isolated zeros* for an analytic function, local version: if a function is
analytic at `z₀`, then either it is identically zero in a neighborhood of `z₀`, or it does not
vanish in a punctured neighborhood of `z₀`. -/
theorem eventually_eq_zero_or_eventually_ne_zero (hf : AnalyticAt 𝕜 f z₀) :
(∀ᶠ z in 𝓝 z₀, f z = 0) ∨ ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
by
rcases hf with ⟨p, hp⟩
by_cases h : p = 0
· exact Or.inl (HasFPowerSeriesAt.eventually_eq_zero (by rwa [h] at hp))
· exact Or.inr (hp.locally_ne_zero h)
