Theorem MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotent

Modification history

2025-04-07 21:54
Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
feat: golf, generalize and review API for topological nilpotency of power series (#23683) …
Added MvPowerSeries.WithPiTopology.isTopologicallyNilpotent_of_constantCoeff_isNilpotentView on Github →