Mathlib Changelog
v4
Changelog
About
Github
Theorem
MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff
Modification history
2025-04-07 21:54
Mathlib/RingTheory/MvPowerSeries/LinearTopology.lean
feat: golf, generalize and review API for topological nilpotency of power series (#23683) …
Added
MvPowerSeries.LinearTopology.isTopologicallyNilpotent_of_constantCoeff
View on Github →