Commit 2025-11-21 12:10 588a7513

View on Github →

feat(Algebra/Polynomial): misc lemma about mod (#31634) Added the following

degree_mod_lt, add_mod, sub_mod, mod_eq_of_dvd_sub: corresponding to existing lemma on modByMonic
mul_mod, mul_modByMonic: similar to Nat.mul_mod

Estimated changes

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Polynomial.mul_modByMonic

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

added theorem Polynomial.add_mod

added theorem Polynomial.degree_mod_lt

added theorem Polynomial.mod_eq_of_dvd_sub

added theorem Polynomial.mul_mod

added theorem Polynomial.sub_mod