Theorem Commute.pow_dvd_sub_pow_of_pow_eq_zero_right

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_sub_pow_of_pow_eq_zero_rightView 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_sub_pow_of_pow_eq_zero_rightView on Github →