isTopologicallyNilpotent_of_constantCoeff_zero

English

If the constantCoeff is zero, then f^n → 0 as n → ∞ in the atTop topology.

Русский

Если константный коэффициент равен нулю, то f^n сходится к 0 при n → ∞ в топологии atTop.

LaTeX

$$constantCoeff f = 0 → Tendsto (λ n, f^n) atTop (nhds 0)$$

Lean4

theorem isTopologicallyNilpotent_of_constantCoeff_zero [CommSemiring R] {f : MvPowerSeries σ R}
    (hf : constantCoeff f = 0) : Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) :=
  by
  apply isTopologicallyNilpotent_of_constantCoeff_isNilpotent
  rw [hf]
  exact IsNilpotent.zero

Похожие утверждения