isTopologicallyNilpotent_of_constantCoeff_zero

English

If the constant coefficient of a power series f is zero, then f^n tends to zero in the Pi-topology.

Русский

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

LaTeX

$$$\mathrm{constantCoeff}(f) = 0 \Rightarrow \mathrm{Tendsto}(n \mapsto f^n)\;\to\; 0$$$

Lean4

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

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