Theorems · Theorem · commutative algebra

MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent

∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : CommRing R] [DiscreteTopology R]
  (f : MvPowerSeries σ R), IsTopologicallyNilpotent f ↔ IsNilpotent (MvPowerSeries.constantCoeff f)

Assuming the base ring has a discrete topology, the powers of a MvPowerSeries converge to 0 iff its constant coefficient is nilpotent. [N. Bourbaki, Algebra II, Chapter 4, §4, n°2, corollary of prop. 3][bourbaki1981] See also MvPowerSeries.LinearTopology.isTopologicallyNilpotent_iff_constantCoeff.

Defined in

Mathlib.RingTheory.MvPowerSeries.PiTopology

Cited by

1 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCommRingDiscreteTopology