Commit 2023-03-19 06:36 c5000556

View on Github →

feat: port Data.Polynomial.Div (#2975)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Div.lean

added theorem Polynomial.X_dvd_iff

added theorem Polynomial.X_pow_dvd_iff

added def Polynomial.decidableDvdMonic

added theorem Polynomial.degree_add_divByMonic

added theorem Polynomial.degree_divByMonic_le

added theorem Polynomial.degree_divByMonic_lt

added theorem Polynomial.degree_modByMonic_le

added theorem Polynomial.degree_modByMonic_lt

added def Polynomial.divByMonic

added theorem Polynomial.divByMonic_eq_of_not_monic

added theorem Polynomial.divByMonic_eq_zero_iff

added theorem Polynomial.divByMonic_mul_pow_rootMultiplicity_eq

added theorem Polynomial.divByMonic_one

added theorem Polynomial.divByMonic_zero

added theorem Polynomial.div_modByMonic_unique

added theorem Polynomial.div_wf_lemma

added theorem Polynomial.dvd_iff_isRoot

added theorem Polynomial.dvd_iff_modByMonic_eq_zero

added theorem Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero

added theorem Polynomial.eval₂_modByMonic_eq_self_of_root

added theorem Polynomial.ker_evalRingHom

added theorem Polynomial.map_divByMonic

added theorem Polynomial.map_dvd_map

added theorem Polynomial.map_modByMonic

added theorem Polynomial.map_mod_divByMonic

added def Polynomial.modByMonic

added theorem Polynomial.modByMonic_X

added theorem Polynomial.modByMonic_X_sub_C_eq_C_eval

added theorem Polynomial.modByMonic_add_div

added theorem Polynomial.modByMonic_eq_of_not_monic

added theorem Polynomial.modByMonic_eq_self_iff

added theorem Polynomial.modByMonic_eq_sub_mul_div

added theorem Polynomial.modByMonic_one

added theorem Polynomial.modByMonic_zero

added theorem Polynomial.mul_divByMonic_eq_iff_isRoot

added theorem Polynomial.mul_div_mod_by_monic_cancel_left

added theorem Polynomial.multiplicity_X_sub_C_finite

added theorem Polynomial.multiplicity_finite_of_degree_pos_of_monic

added theorem Polynomial.natDegree_divByMonic

added theorem Polynomial.not_isField

added theorem Polynomial.pow_rootMultiplicity_dvd

added def Polynomial.rootMultiplicity

added theorem Polynomial.rootMultiplicity_C

added theorem Polynomial.rootMultiplicity_eq_multiplicity

added theorem Polynomial.rootMultiplicity_eq_zero

added theorem Polynomial.rootMultiplicity_eq_zero_iff

added theorem Polynomial.rootMultiplicity_pos'

added theorem Polynomial.rootMultiplicity_pos

added theorem Polynomial.rootMultiplicity_zero

added theorem Polynomial.sub_dvd_eval_sub

added theorem Polynomial.sum_modByMonic_coeff

added theorem Polynomial.zero_divByMonic

added theorem Polynomial.zero_modByMonic