Theorem isRadical_iff_pow_one_lt

Modification history

2025-04-08 21:08
Mathlib/RingTheory/Nilpotent/Defs.lean
feat: generalize half of Mathlib.RingTheory (#23173) …
Modified isRadical_iff_pow_one_ltView on Github →
2024-04-23 14:29
Mathlib/RingTheory/Nilpotent.lean
chore: split RingTheory.Nilpotent (#12184) …
Modified isRadical_iff_pow_one_ltView on Github →
2023-03-12 19:12
Mathlib/RingTheory/Nilpotent.lean
feat: port RingTheory.Nilpotent (#2829)
Added isRadical_iff_pow_one_ltView on Github →