Theorem IsNilpotent.pow_of_pos

Modification history

2024-04-23 14:29

Mathlib/RingTheory/Nilpotent.lean

chore: split RingTheory.Nilpotent (#12184) …

Modified IsNilpotent.pow_of_pos View on Github →

2023-09-25 14:23

Mathlib/RingTheory/Nilpotent.lean

feat(RingTheory/Nilpotent): add lemma on powers of nilpotents (#7340) …

Added IsNilpotent.pow_of_pos View on Github →