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