Commit 2023-03-23 14:06 667f2856

View on Github →

feat port:Data.Polynomial.RingDivision (#3029)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Polynomial/Div.lean

added theorem Polynomial.rootMultiplicity_eq_nat_find_of_nonzero

Created Mathlib/Data/Polynomial/RingDivision.lean

added theorem Multiset.prod_X_sub_C_dvd_iff_le_roots

added theorem Polynomial.Monic.comp

added theorem Polynomial.Monic.comp_X_add_C

added theorem Polynomial.Monic.comp_X_sub_C

added theorem Polynomial.Monic.irreducible_iff_natDegree'

added theorem Polynomial.Monic.irreducible_iff_natDegree

added theorem Polynomial.Monic.irreducible_of_degree_eq_one

added theorem Polynomial.Monic.irreducible_of_irreducible_map

added theorem Polynomial.Monic.not_irreducible_iff_exists_add_mul_eq_coeff

added theorem Polynomial.Monic.prime_of_degree_eq_one

added theorem Polynomial.add_modByMonic

added theorem Polynomial.aeval_eq_zero_of_mem_rootSet

added theorem Polynomial.aeval_modByMonic_eq_self_of_root

added theorem Polynomial.bUnion_roots_finite

added theorem Polynomial.c_leadingCoeff_mul_prod_multiset_X_sub_C

added theorem Polynomial.card_le_degree_of_subset_roots

added theorem Polynomial.card_nthRoots

added theorem Polynomial.card_roots'

added theorem Polynomial.card_roots

added theorem Polynomial.card_roots_X_pow_sub_C

added theorem Polynomial.card_roots_le_map

added theorem Polynomial.card_roots_le_map_of_injective

added theorem Polynomial.card_roots_sub_C'

added theorem Polynomial.card_roots_sub_C

added theorem Polynomial.coeff_coe_units_zero_ne_zero

added theorem Polynomial.comp_eq_zero_iff

added theorem Polynomial.count_map_roots

added theorem Polynomial.count_map_roots_of_injective

added theorem Polynomial.count_roots

added theorem Polynomial.degree_coe_units

added theorem Polynomial.degree_eq_degree_of_associated

added theorem Polynomial.degree_eq_one_of_irreducible_of_root

added theorem Polynomial.degree_eq_zero_of_isUnit

added theorem Polynomial.degree_le_mul_left

added theorem Polynomial.degree_le_of_dvd

added theorem Polynomial.degree_pos_of_aeval_root

added theorem Polynomial.eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le

added theorem Polynomial.eq_of_infinite_eval_eq

added theorem Polynomial.eq_of_monic_of_associated

added theorem Polynomial.eq_of_monic_of_dvd_of_natDegree_le

added theorem Polynomial.eq_rootMultiplicity_map

added theorem Polynomial.eq_zero_of_dvd_of_degree_lt

added theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt

added theorem Polynomial.eq_zero_of_infinite_isRoot

added theorem Polynomial.exists_max_root

added theorem Polynomial.exists_min_root

added theorem Polynomial.exists_multiset_roots

added theorem Polynomial.exists_prod_multiset_X_sub_C_mul

added theorem Polynomial.finite_setOf_isRoot

added theorem Polynomial.funext

added theorem Polynomial.irreducible_X

added theorem Polynomial.irreducible_X_sub_C

added theorem Polynomial.irreducible_of_monic

added theorem Polynomial.isCoprime_X_sub_C_of_isUnit_sub

added theorem Polynomial.isRoot_of_mem_roots

added theorem Polynomial.isUnit_iff

added theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map

added theorem Polynomial.le_rootMultiplicity_iff

added theorem Polynomial.le_rootMultiplicity_map

added theorem Polynomial.leadingCoeff_divByMonic_X_sub_C

added theorem Polynomial.leadingCoeff_divByMonic_of_monic

added theorem Polynomial.map_roots_le

added theorem Polynomial.map_roots_le_of_injective

added theorem Polynomial.mem_nthRoots

added theorem Polynomial.mem_nthRootsFinset

added theorem Polynomial.mem_rootSet'

added theorem Polynomial.mem_rootSet

added theorem Polynomial.mem_rootSet_of_ne

added theorem Polynomial.mem_roots'

added theorem Polynomial.mem_roots

added theorem Polynomial.mem_roots_sub_C'

added theorem Polynomial.mem_roots_sub_C

added def Polynomial.modByMonicHom

added theorem Polynomial.modByMonic_eq_of_dvd_sub

added theorem Polynomial.monic_prod_multiset_X_sub_C

added theorem Polynomial.natDegree_coe_units

added theorem Polynomial.natDegree_eq_zero_of_isUnit

added theorem Polynomial.natDegree_le_of_dvd

added theorem Polynomial.natDegree_mul

added theorem Polynomial.natDegree_multiset_prod_X_sub_C_eq_card

added theorem Polynomial.natDegree_pos_of_aeval_root

added theorem Polynomial.natDegree_pow

added theorem Polynomial.natDegree_sub_eq_of_prod_eq

added theorem Polynomial.ne_zero_of_mem_rootSet

added theorem Polynomial.ne_zero_of_mem_roots

added theorem Polynomial.not_dvd_of_degree_lt

added theorem Polynomial.not_dvd_of_natDegree_lt

added def Polynomial.nthRoots

added def Polynomial.nthRootsFinset

added theorem Polynomial.nthRootsFinset_zero

added theorem Polynomial.nthRoots_two_eq_zero_iff

added theorem Polynomial.nthRoots_zero

added theorem Polynomial.pairwise_coprime_X_sub_C

added theorem Polynomial.pow_rootMultiplicity_not_dvd

added theorem Polynomial.prime_X

added theorem Polynomial.prime_X_sub_C

added theorem Polynomial.prod_multiset_X_sub_C_dvd

added theorem Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq

added theorem Polynomial.prod_multiset_root_eq_finset_root

added theorem Polynomial.rootMultiplicity_X_sub_C

added theorem Polynomial.rootMultiplicity_X_sub_C_pow

added theorem Polynomial.rootMultiplicity_X_sub_C_self

added theorem Polynomial.rootMultiplicity_add

added theorem Polynomial.rootMultiplicity_le_iff

added theorem Polynomial.rootMultiplicity_mul

added def Polynomial.rootSet

added theorem Polynomial.rootSet_C

added theorem Polynomial.rootSet_def

added theorem Polynomial.rootSet_finite

added theorem Polynomial.rootSet_mapsTo

added theorem Polynomial.rootSet_maps_to'

added theorem Polynomial.rootSet_zero

added theorem Polynomial.root_mul

added theorem Polynomial.root_or_root_of_root_mul

added theorem Polynomial.roots.le_of_dvd

added theorem Polynomial.roots_C

added theorem Polynomial.roots_C_mul

added theorem Polynomial.roots_C_mul_X_pow

added theorem Polynomial.roots_X

added theorem Polynomial.roots_X_pow

added theorem Polynomial.roots_X_sub_C

added theorem Polynomial.roots_list_prod

added theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree

added theorem Polynomial.roots_monomial

added theorem Polynomial.roots_mul

added theorem Polynomial.roots_multiset_prod

added theorem Polynomial.roots_multiset_prod_X_sub_C

added theorem Polynomial.roots_one

added theorem Polynomial.roots_pow

added theorem Polynomial.roots_prod

added theorem Polynomial.roots_prod_X_sub_C

added theorem Polynomial.roots_smul_nonzero

added theorem Polynomial.roots_zero

added theorem Polynomial.smul_modByMonic

added theorem Polynomial.trailingDegree_mul

added theorem Polynomial.units_coeff_zero_smul

added theorem Polynomial.zero_of_eval_zero