Def Polynomial.divByMonicHom

Modification history

2026-09-01 18:09

Mathlib/Algebra/Polynomial/RingDivision.lean

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

Added Polynomial.divByMonicHom View on Github →