Commit 2024-03-24 09:17 f16daa68
View on Github →feat: Polynomial.mul_modByMonic (#11113)
Adds simp lemma for (p * q) %ₘ q = 0
and (q * p) %ₘ q = 0
.
Also corrects a misspelling: dvd_iff_modByMonic_eq_zero
should be modByMonic_eq_zero_iff_dvd
feat: Polynomial.mul_modByMonic (#11113)
Adds simp lemma for (p * q) %ₘ q = 0
and (q * p) %ₘ q = 0
.
Also corrects a misspelling: dvd_iff_modByMonic_eq_zero
should be modByMonic_eq_zero_iff_dvd