Commit 2023-03-24 17:26 61e4cecb

View on Github →

feat: port Data.Polynomial.FieldDivision (#3057)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/FieldDivision.lean

added theorem Polynomial.C_mul_dvd

added theorem Polynomial.Monic.normalize_eq_self

added theorem Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic

added theorem Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic

added theorem Polynomial.coe_normUnit

added theorem Polynomial.coe_normUnit_of_ne_zero

added theorem Polynomial.coeff_inv_units

added theorem Polynomial.degree_add_div

added theorem Polynomial.degree_div_le

added theorem Polynomial.degree_div_lt

added theorem Polynomial.degree_map

added theorem Polynomial.degree_mul_leadingCoeff_inv

added theorem Polynomial.degree_normalize

added theorem Polynomial.degree_pos_of_irreducible

added theorem Polynomial.degree_pos_of_ne_zero_of_nonunit

added theorem Polynomial.derivative_rootMultiplicity_of_root

added def Polynomial.div

added theorem Polynomial.divByMonic_add_X_Sub_C_mul_derivate_divByMonic_eq_derivative

added theorem Polynomial.divByMonic_eq_div

added theorem Polynomial.div_C_mul

added theorem Polynomial.div_def

added theorem Polynomial.div_eq_zero_iff

added theorem Polynomial.dvd_C_mul

added theorem Polynomial.eval_gcd_eq_zero

added theorem Polynomial.eval₂_gcd_eq_zero

added theorem Polynomial.exists_root_of_degree_eq_one

added theorem Polynomial.gcd_map

added theorem Polynomial.irreducible_of_degree_eq_one

added theorem Polynomial.isCoprime_map

added theorem Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero

added theorem Polynomial.isRoot_gcd_iff_isRoot_left_right

added theorem Polynomial.isUnit_iff_degree_eq_zero

added theorem Polynomial.isUnit_map

added theorem Polynomial.leadingCoeff_div

added theorem Polynomial.leadingCoeff_map

added theorem Polynomial.leadingCoeff_normalize

added theorem Polynomial.map_div

added theorem Polynomial.map_dvd_map'

added theorem Polynomial.map_eq_zero

added theorem Polynomial.map_mod

added theorem Polynomial.map_ne_zero

added theorem Polynomial.mem_roots_map

added def Polynomial.mod

added theorem Polynomial.modByMonic_eq_mod

added theorem Polynomial.mod_def

added theorem Polynomial.mod_eq_self_iff

added theorem Polynomial.mod_x_sub_c_eq_c_eval

added theorem Polynomial.monic_map_iff

added theorem Polynomial.monic_mul_leadingCoeff_inv

added theorem Polynomial.monic_normalize

added theorem Polynomial.mul_div_eq_iff_isRoot

added theorem Polynomial.natDegree_map

added theorem Polynomial.normalize_monic

added theorem Polynomial.not_irreducible_c

added theorem Polynomial.prime_of_degree_eq_one

added theorem Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity

added theorem Polynomial.rootSet_C_mul_X_pow

added theorem Polynomial.rootSet_X_pow

added theorem Polynomial.rootSet_monomial

added theorem Polynomial.rootSet_prod

added theorem Polynomial.root_gcd_iff_root_left_right

added theorem Polynomial.root_left_of_root_gcd

added theorem Polynomial.root_right_of_root_gcd

added theorem Polynomial.roots_normalize