Theorem Commute.add_pow_dvd_pow_of_pow_eq_zero_left

Modification history

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