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