English
Let f be a mv-power-series. Then f tends to 0 under powers if and only if its constant coefficient is topologically nilpotent.
Русский
Пусть f — mv-ряд. Тогда f^{n} → 0 тогда и только если его константный коэффициент топологически нильпотентен.
LaTeX
$$$\displaystyle \operatorname{Tendsto}(n\mapsto f^{n})\_{{\mathrm{atTop}}}\, (\nhds 0) \iff \operatorname{IsTopologicallyNilpotent}(\mathrm{constantCoeff}(f)).$$$
Lean4
/-- Assuming the base ring has a linear topology, the powers of a `MvPowerSeries` converge to 0
iff its constant coefficient is topologically nilpotent.
See also `MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent`. -/
theorem isTopologicallyNilpotent_iff_constantCoeff {R : Type*} [CommRing R] [TopologicalSpace R] [IsLinearTopology R R]
(f : MvPowerSeries σ R) :
Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) ↔ IsTopologicallyNilpotent (constantCoeff f) :=
by
refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff⟩
replace H : Tendsto (fun n ↦ constantCoeff (f ^ n)) atTop (nhds 0) :=
continuous_constantCoeff R |>.tendsto' 0 0 constantCoeff_zero |>.comp H
simpa only [map_pow] using H
