Theorems · Theorem · commutative algebra

PowerSeries.WithPiTopology.isTopologicallyNilpotent_iff_constantCoeff_isNilpotent

∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : CommRing R] [DiscreteTopology R] (f : PowerSeries R),
  Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0) ↔ IsNilpotent (PowerSeries.constantCoeff f)

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]

Defined in

Mathlib.RingTheory.PowerSeries.PiTopology

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceCommRingDiscreteTopology