Theorem not_isNilpotent_one

Modification history

2026-01-13 09:55
Mathlib/Algebra/GroupWithZero/Basic.lean
chore(Algebra): deduplicate `IsReduced` lemmas (#33775) …
Modified not_isNilpotent_oneView on Github →
2024-04-23 14:29
Mathlib/RingTheory/Nilpotent.lean
chore: split RingTheory.Nilpotent (#12184) …
Modified not_isNilpotent_oneView on Github →
2023-11-27 17:05
Mathlib/RingTheory/Nilpotent.lean
feat: Add `not_isNilpotent_one`. (#8648)
Added not_isNilpotent_oneView on Github →