Commit 2023-12-06 21:57 796fc3fc

View on Github →

feat : add lemma on nilpotent and powers (#8831) Changed IsNilpotent.pow to IsNilpotent.pow_succ. Added IsNilpotent.of_pow and IsNilpotent.pow_iff_pos.

Estimated changes

Modified Mathlib/RingTheory/Nilpotent.lean

added theorem IsNilpotent.of_pow

deleted theorem IsNilpotent.pow

added theorem IsNilpotent.pow_iff_pos

added theorem IsNilpotent.pow_succ