Theorem Commute.IsNilpotent.add_isUnit

Modification history

2024-02-06 16:43
Mathlib/RingTheory/Nilpotent.lean
feat: define Newton's method and prove decomposition as nilpotent + root (#10284) …
Deleted Commute.IsNilpotent.add_isUnitView on Github →
2023-07-04 09:34
Mathlib/RingTheory/Nilpotent.lean
feat: units of polynomial rings (#4691) …
Added Commute.IsNilpotent.add_isUnitView on Github →