Theorem Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero
Modification history
2024-07-25 23:15
Mathlib/RingTheory/Nilpotent/Basic.lean
Chore: robustifying for debug.byAsSorry (part 7) (#15137) …
Modified Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zeroView on Github →