Theorem Commute.pow_dvd_pow_of_sub_pow_eq_zero

Modification history

2024-07-25 23:15
Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
Chore: robustifying for debug.byAsSorry (part 7) (#15137) …
Modified Commute.pow_dvd_pow_of_sub_pow_eq_zeroView on Github →
2023-09-26 09:02
Mathlib/Algebra/Ring/Divisibility/Lemmas.lean
feat: lemmas about divisibility, mostly related to nilpotency (#7355)
Added Commute.pow_dvd_pow_of_sub_pow_eq_zeroView on Github →