isTopologicallyNilpotent_of_constantCoeff_isNilpotent

English

If the constant coefficient of a power series f ∈ PowerSeries(R) is nilpotent in a CommSemiring R, then the powers f^n converge to 0 in the Pi-topology.

Русский

Если константный коэффициент степенного ряда f ∈ PowerSeries(R) нильпотентен в коммутативном полугруппе, то степени f^n сходятся к 0 в топологии Pi.

LaTeX

$$$\mathrm{IsNilpotent}(\mathrm{constantCoeff}(f)) \Rightarrow \mathrm{Tendsto}(n \mapsto f^n)\;{\to}\; 0\;\text{in atTop nhds}$$$

Lean4

theorem isTopologicallyNilpotent_of_constantCoeff_isNilpotent [CommSemiring R] {f : PowerSeries R}
    (hf : IsNilpotent (constantCoeff (R := R) f)) : Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) :=
  MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent hf

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