English
A locally zero formal power series around z0 is equivalent to the associated coefficient vanishing across a neighborhood; the analytic structure forces identity.
Русский
Условие локальной нулевой силы формальной степенной серии вблизи z0 эквивалентно нулю соответствующих коэффициентов; аналитическая структура вызывает тождество.
LaTeX
$$$\text{locally_zero_iff}$: HasFPowerSeriesAt f p z0 \Longleftrightarrow p = 0$$
Lean4
theorem locally_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) : ∀ᶠ z in 𝓝[≠] z₀, f z ≠ 0 :=
by
rw [eventually_nhdsWithin_iff]
have h2 := (has_fpower_series_iterate_dslope_fslope p.order hp).continuousAt
have h3 := h2.eventually_ne (iterate_dslope_fslope_ne_zero hp h)
filter_upwards [eq_pow_order_mul_iterate_dslope hp, h3] with z e1 e2 e3
simpa [e1, e2, e3] using pow_ne_zero p.order (sub_ne_zero.mpr e3)
