Commit 2025-03-18 18:59 609bae75

View on Github →

chore: rename IsNilpotent.exp_of_nilpotent_is_unit (#22822)

Estimated changes

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

deleted theorem IsNilpotent.exp_of_nilpotent_is_unit

added theorem IsNilpotent.isUnit_exp