isTopologicallyNilpotent_iff_constantCoeff_isNilpotent

English

Let R be a CommRing with the discrete topology. Then Tendsto (f^n) to 0 in PowerSeries(R) if and only if the constant coefficient of f is nilpotent.

Русский

Пусть R — коммутативное кольцо с дискретной топологией. Тогда $f^n \to 0$ в PowerSeries(R) тогда и только тогда, когда константный коэффициент f нильпотентен.

LaTeX

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

Lean4

/-- Assuming the base ring has a discrete topology, the powers of a `PowerSeries` converge to 0
iff its constant coefficient is nilpotent.
[N. Bourbaki, *Algebra {II}*, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] -/
theorem isTopologicallyNilpotent_iff_constantCoeff_isNilpotent [CommRing R] [DiscreteTopology R] (f : PowerSeries R) :
    Tendsto (fun n : ℕ => f ^ n) atTop (nhds 0) ↔ IsNilpotent (constantCoeff f) :=
  MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent f

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