Commit 2024-05-18 20:54 dd53bf00

View on Github →

refactor(Algebra.Polynomial.RingDivision): split large file (#12958) Currently Algebra.Polynomial.RingDivision is a strange mix of basic results about polynomial rings and stuff about their roots. We move those to a new file Algebra.Polynomial.Roots.

Estimated changes

Modified Archive/Imo/Imo2006Q5.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/RingDivision.lean

deleted theorem Multiset.prod_X_sub_C_dvd_iff_le_roots

deleted theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C

deleted theorem Polynomial.Monic.irreducible_iff_degree_lt

deleted theorem Polynomial.Monic.isUnit_leadingCoeff_of_dvd

deleted theorem Polynomial.aeval_eq_zero_of_mem_rootSet

deleted theorem Polynomial.aroots_C

deleted theorem Polynomial.aroots_C_mul

deleted theorem Polynomial.aroots_C_mul_X_pow

deleted theorem Polynomial.aroots_X

deleted theorem Polynomial.aroots_X_pow

deleted theorem Polynomial.aroots_X_sub_C

deleted theorem Polynomial.aroots_def

deleted theorem Polynomial.aroots_monomial

deleted theorem Polynomial.aroots_mul

deleted theorem Polynomial.aroots_neg

deleted theorem Polynomial.aroots_one

deleted theorem Polynomial.aroots_pow

deleted theorem Polynomial.aroots_smul_nonzero

deleted theorem Polynomial.aroots_zero

deleted theorem Polynomial.bUnion_roots_finite

deleted theorem Polynomial.card_le_degree_of_subset_roots

deleted theorem Polynomial.card_nthRoots

deleted theorem Polynomial.card_roots'

deleted theorem Polynomial.card_roots

deleted theorem Polynomial.card_roots_X_pow_sub_C

deleted theorem Polynomial.card_roots_le_map

deleted theorem Polynomial.card_roots_le_map_of_injective

deleted theorem Polynomial.card_roots_sub_C'

deleted theorem Polynomial.card_roots_sub_C

deleted theorem Polynomial.count_map_roots

deleted theorem Polynomial.count_map_roots_of_injective

deleted theorem Polynomial.count_roots

deleted theorem Polynomial.eq_of_infinite_eval_eq

deleted theorem Polynomial.eq_rootMultiplicity_map

deleted theorem Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card

deleted theorem Polynomial.eq_zero_of_infinite_isRoot

deleted theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero'

deleted theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero

deleted theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card

deleted theorem Polynomial.exists_max_root

deleted theorem Polynomial.exists_min_root

deleted theorem Polynomial.exists_prod_multiset_X_sub_C_mul

deleted theorem Polynomial.finite_setOf_isRoot

deleted theorem Polynomial.funext

deleted theorem Polynomial.isRoot_of_mem_roots

deleted theorem Polynomial.le_rootMultiplicity_map

deleted theorem Polynomial.map_roots_le

deleted theorem Polynomial.map_roots_le_of_injective

deleted theorem Polynomial.mem_aroots'

deleted theorem Polynomial.mem_aroots

deleted theorem Polynomial.mem_nthRoots

deleted theorem Polynomial.mem_nthRootsFinset

deleted theorem Polynomial.mem_rootSet'

deleted theorem Polynomial.mem_rootSet

deleted theorem Polynomial.mem_rootSet_of_ne

deleted theorem Polynomial.mem_roots'

deleted theorem Polynomial.mem_roots

deleted theorem Polynomial.mem_roots_iff_aeval_eq_zero

deleted theorem Polynomial.mem_roots_sub_C'

deleted theorem Polynomial.mem_roots_sub_C

deleted theorem Polynomial.monic_prod_multiset_X_sub_C

deleted theorem Polynomial.mul_mem_nthRootsFinset

deleted theorem Polynomial.ne_zero_of_mem_nthRootsFinset

deleted theorem Polynomial.ne_zero_of_mem_rootSet

deleted theorem Polynomial.ne_zero_of_mem_roots

deleted def Polynomial.nthRoots

deleted def Polynomial.nthRootsFinset

deleted theorem Polynomial.nthRootsFinset_def

deleted theorem Polynomial.nthRootsFinset_zero

deleted theorem Polynomial.nthRoots_two_eq_zero_iff

deleted theorem Polynomial.nthRoots_zero

deleted theorem Polynomial.nthRoots_zero_right

deleted theorem Polynomial.one_mem_nthRootsFinset

deleted theorem Polynomial.prod_multiset_X_sub_C_dvd

deleted theorem Polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq

deleted theorem Polynomial.prod_multiset_root_eq_finset_root

deleted def Polynomial.rootSet

deleted theorem Polynomial.rootSet_C

deleted theorem Polynomial.rootSet_def

deleted theorem Polynomial.rootSet_finite

deleted theorem Polynomial.rootSet_mapsTo

deleted theorem Polynomial.rootSet_maps_to'

deleted theorem Polynomial.rootSet_neg

deleted theorem Polynomial.rootSet_one

deleted theorem Polynomial.rootSet_zero

deleted theorem Polynomial.roots.le_of_dvd

deleted theorem Polynomial.roots_C

deleted theorem Polynomial.roots_C_mul

deleted theorem Polynomial.roots_C_mul_X_pow

deleted theorem Polynomial.roots_X

deleted theorem Polynomial.roots_X_pow

deleted theorem Polynomial.roots_X_sub_C

deleted theorem Polynomial.roots_def

deleted theorem Polynomial.roots_list_prod

deleted theorem Polynomial.roots_map_of_injective_of_card_eq_natDegree

deleted theorem Polynomial.roots_monomial

deleted theorem Polynomial.roots_mul

deleted theorem Polynomial.roots_multiset_prod

deleted theorem Polynomial.roots_multiset_prod_X_sub_C

deleted theorem Polynomial.roots_neg

deleted theorem Polynomial.roots_one

deleted theorem Polynomial.roots_pow

deleted theorem Polynomial.roots_prod

deleted theorem Polynomial.roots_prod_X_sub_C

deleted theorem Polynomial.roots_smul_nonzero

deleted theorem Polynomial.roots_zero

deleted theorem Polynomial.zero_of_eval_zero

Created Mathlib/Algebra/Polynomial/Roots.lean

added theorem Multiset.prod_X_sub_C_dvd_iff_le_roots

added theorem Polynomial.C_leadingCoeff_mul_prod_multiset_X_sub_C

added theorem Polynomial.Monic.irreducible_iff_degree_lt

added theorem Polynomial.Monic.isUnit_leadingCoeff_of_dvd

added theorem Polynomial.aeval_eq_zero_of_mem_rootSet

added theorem Polynomial.aroots_C

added theorem Polynomial.aroots_C_mul

added theorem Polynomial.aroots_C_mul_X_pow

added theorem Polynomial.aroots_X

added theorem Polynomial.aroots_X_pow

added theorem Polynomial.aroots_X_sub_C

added theorem Polynomial.aroots_def

added theorem Polynomial.aroots_monomial

added theorem Polynomial.aroots_mul

added theorem Polynomial.aroots_neg

added theorem Polynomial.aroots_one

added theorem Polynomial.aroots_pow

added theorem Polynomial.aroots_smul_nonzero

added theorem Polynomial.aroots_zero

added theorem Polynomial.bUnion_roots_finite

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.count_map_roots

added theorem Polynomial.count_map_roots_of_injective

added theorem Polynomial.count_roots

added theorem Polynomial.eq_of_infinite_eval_eq

added theorem Polynomial.eq_rootMultiplicity_map

added theorem Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card

added theorem Polynomial.eq_zero_of_infinite_isRoot

added theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero'

added theorem Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero

added theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card

added theorem Polynomial.exists_max_root

added theorem Polynomial.exists_min_root

added theorem Polynomial.exists_prod_multiset_X_sub_C_mul

added theorem Polynomial.finite_setOf_isRoot

added theorem Polynomial.funext

added theorem Polynomial.isRoot_of_mem_roots

added theorem Polynomial.le_rootMultiplicity_map

added theorem Polynomial.map_roots_le

added theorem Polynomial.map_roots_le_of_injective

added theorem Polynomial.mem_aroots'

added theorem Polynomial.mem_aroots

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_iff_aeval_eq_zero

added theorem Polynomial.mem_roots_sub_C'

added theorem Polynomial.mem_roots_sub_C

added theorem Polynomial.monic_prod_multiset_X_sub_C

added theorem Polynomial.mul_mem_nthRootsFinset

added theorem Polynomial.ne_zero_of_mem_nthRootsFinset

added theorem Polynomial.ne_zero_of_mem_rootSet

added theorem Polynomial.ne_zero_of_mem_roots

added def Polynomial.nthRoots

added def Polynomial.nthRootsFinset

added theorem Polynomial.nthRootsFinset_def

added theorem Polynomial.nthRootsFinset_zero

added theorem Polynomial.nthRoots_two_eq_zero_iff

added theorem Polynomial.nthRoots_zero

added theorem Polynomial.nthRoots_zero_right

added theorem Polynomial.one_mem_nthRootsFinset

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 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_neg

added theorem Polynomial.rootSet_one

added theorem Polynomial.rootSet_zero

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_def

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_neg

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.zero_of_eval_zero

Modified Mathlib/Algebra/Polynomial/SpecificDegree.lean

Modified Mathlib/Analysis/SpecialFunctions/Polynomials.lean

Modified Mathlib/RingTheory/Binomial.lean

Modified Mathlib/RingTheory/IntegralDomain.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified scripts/style-exceptions.txt