Theorem IsNilpotent.of_pow

Modification history

2026-01-13 09:55
Mathlib/Algebra/GroupWithZero/Basic.lean
chore(Algebra): deduplicate `IsReduced` lemmas (#33775) …
Modified IsNilpotent.of_powView on Github →
2025-02-02 22:26
Mathlib/RingTheory/Nilpotent/Defs.lean
chore: tidy various files (#20225)
Modified IsNilpotent.of_powView on Github →
2024-04-23 14:29
Mathlib/RingTheory/Nilpotent.lean
chore: split RingTheory.Nilpotent (#12184) …
Modified IsNilpotent.of_powView on Github →
2023-12-06 21:57
Mathlib/RingTheory/Nilpotent.lean
feat : add lemma on nilpotent and powers (#8831) …
Added IsNilpotent.of_powView on Github →