Commit 2026-09-01 22:08 bfe34f17

View on Github →

chore(Algebra/Polynomial/Div): generalize rootMultiplicity lemmas to non-commutative rings (#43279)

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

modified theorem Polynomial.comp_X_add_C_eq_zero_iff

modified theorem Polynomial.comp_X_add_C_ne_zero_iff

Modified Mathlib/Algebra/Polynomial/Div.lean