Commit 2026-09-01 18:09 8fc07d3b

View on Github →

feat(Algebra/Polynomial): linearity of divByMonic and adjacent results (#39868)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Div.lean

added theorem Polynomial.add_divByMonic

modified theorem Polynomial.add_modByMonic

added theorem Polynomial.mul_divByMonic_assoc

added theorem Polynomial.neg_divByMonic

added theorem Polynomial.sub_divByMonic

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

added def Polynomial.divByMonicHom

added theorem Polynomial.mem_ker_divByMonic

added theorem Polynomial.smul_divByMonic

modified theorem Polynomial.smul_modByMonic