Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-12-08 09:33
64c626ab
View on Github →
chore: generalize Polynomial.Div to noncommutative rings (
#8889
)
Estimated changes
Modified
Mathlib/Data/Polynomial/Div.lean
deleted
theorem
Polynomial.divByMonic_mul_pow_rootMultiplicity_eq
modified
theorem
Polynomial.map_divByMonic
modified
theorem
Polynomial.map_dvd_map
modified
theorem
Polynomial.map_modByMonic
modified
theorem
Polynomial.map_mod_divByMonic
modified
theorem
Polynomial.natDegree_divByMonic
added
theorem
Polynomial.pow_mul_divByMonic_rootMultiplicity_eq
Modified
Mathlib/Data/Polynomial/FieldDivision.lean