Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-09 06:40 6a5a6494

View on Github →

chore(field_theory): move polynomial.splits to a new file (#17354) I noticed a lot of files use polynomial.splits without needing splitting_field. Since the definition of splits has a lot less dependencies than splitting_field, splitting the splitting field file hopefully helps recompilation a bit. The new files are:

data.polynomial.splits: definition of polynomial.splits and all lemmas not mentioning (is_)splitting_field
ring_theory.adjoin.field: some auxiliary lemmas on adjoining elements to a ring that are also used outside of field_theory.splitting_field

Estimated changes

Modified src/algebra/cubic_discriminant.lean

Created src/data/polynomial/splits.lean

added theorem polynomial.adjoin_root_set_eq_range

added theorem polynomial.aeval_root_derivative_of_splits

added theorem polynomial.degree_eq_card_roots'

added theorem polynomial.degree_eq_card_roots

added theorem polynomial.degree_eq_one_of_irreducible_of_splits

added theorem polynomial.eq_X_sub_C_of_splits_of_single_root

added theorem polynomial.eq_prod_roots_of_monic_of_splits_id

added theorem polynomial.eq_prod_roots_of_splits

added theorem polynomial.eq_prod_roots_of_splits_id

added theorem polynomial.exists_root_of_splits'

added theorem polynomial.exists_root_of_splits

added theorem polynomial.image_root_set

added theorem polynomial.map_root_of_splits'

added theorem polynomial.map_root_of_splits

added theorem polynomial.nat_degree_eq_card_roots'

added theorem polynomial.nat_degree_eq_card_roots

added theorem polynomial.prod_roots_eq_coeff_zero_of_monic_of_split

added def polynomial.root_of_splits'

added theorem polynomial.root_of_splits'_eq_root_of_splits

added def polynomial.root_of_splits

added theorem polynomial.roots_map

added theorem polynomial.roots_ne_zero_of_splits'

added theorem polynomial.roots_ne_zero_of_splits

added theorem polynomial.splits.def

added def polynomial.splits

added theorem polynomial.splits_C

added theorem polynomial.splits_X

added theorem polynomial.splits_X_pow

added theorem polynomial.splits_X_sub_C

added theorem polynomial.splits_comp_of_splits

added theorem polynomial.splits_id_iff_splits

added theorem polynomial.splits_iff

added theorem polynomial.splits_iff_card_roots

added theorem polynomial.splits_iff_exists_multiset

added theorem polynomial.splits_map_iff

added theorem polynomial.splits_mul

added theorem polynomial.splits_mul_iff

added theorem polynomial.splits_of_degree_eq_one

added theorem polynomial.splits_of_degree_le_one

added theorem polynomial.splits_of_exists_multiset

added theorem polynomial.splits_of_is_unit

added theorem polynomial.splits_of_map_degree_eq_one

added theorem polynomial.splits_of_map_eq_C

added theorem polynomial.splits_of_nat_degree_eq_one

added theorem polynomial.splits_of_nat_degree_le_one

added theorem polynomial.splits_of_splits_gcd_left

added theorem polynomial.splits_of_splits_gcd_right

added theorem polynomial.splits_of_splits_id

added theorem polynomial.splits_of_splits_mul'

added theorem polynomial.splits_of_splits_mul

added theorem polynomial.splits_of_splits_of_dvd

added theorem polynomial.splits_one

added theorem polynomial.splits_pow

added theorem polynomial.splits_prod

added theorem polynomial.splits_prod_iff

added theorem polynomial.splits_zero

added theorem polynomial.sum_roots_eq_next_coeff_of_monic_of_split

Modified src/field_theory/adjoin.lean

Modified src/field_theory/finite/basic.lean

Modified src/field_theory/is_alg_closed/algebraic_closure.lean

Modified src/field_theory/is_alg_closed/basic.lean

Modified src/field_theory/separable.lean

Modified src/field_theory/splitting_field.lean

deleted def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly

deleted theorem finite_dimensional.of_subalgebra_to_submodule

deleted theorem lift_of_splits

deleted theorem polynomial.adjoin_root_set_eq_range

deleted theorem polynomial.aeval_root_derivative_of_splits

deleted theorem polynomial.degree_eq_card_roots'

deleted theorem polynomial.degree_eq_card_roots

deleted theorem polynomial.degree_eq_one_of_irreducible_of_splits

deleted theorem polynomial.eq_X_sub_C_of_splits_of_single_root

deleted theorem polynomial.eq_prod_roots_of_monic_of_splits_id

deleted theorem polynomial.eq_prod_roots_of_splits

deleted theorem polynomial.eq_prod_roots_of_splits_id

deleted theorem polynomial.exists_root_of_splits'

deleted theorem polynomial.exists_root_of_splits

deleted theorem polynomial.image_root_set

deleted theorem polynomial.map_root_of_splits'

deleted theorem polynomial.map_root_of_splits

deleted theorem polynomial.nat_degree_eq_card_roots'

deleted theorem polynomial.nat_degree_eq_card_roots

deleted theorem polynomial.prod_roots_eq_coeff_zero_of_monic_of_split

deleted def polynomial.root_of_splits'

deleted theorem polynomial.root_of_splits'_eq_root_of_splits

deleted def polynomial.root_of_splits

deleted theorem polynomial.roots_map

deleted theorem polynomial.roots_ne_zero_of_splits'

deleted theorem polynomial.roots_ne_zero_of_splits

deleted theorem polynomial.splits.def

deleted def polynomial.splits

deleted theorem polynomial.splits_C

deleted theorem polynomial.splits_X

deleted theorem polynomial.splits_X_pow

deleted theorem polynomial.splits_X_sub_C

deleted theorem polynomial.splits_comp_of_splits

deleted theorem polynomial.splits_id_iff_splits

deleted theorem polynomial.splits_iff

deleted theorem polynomial.splits_iff_card_roots

deleted theorem polynomial.splits_iff_exists_multiset

deleted theorem polynomial.splits_map_iff

deleted theorem polynomial.splits_mul

deleted theorem polynomial.splits_mul_iff

deleted theorem polynomial.splits_of_degree_eq_one

deleted theorem polynomial.splits_of_degree_le_one

deleted theorem polynomial.splits_of_exists_multiset

deleted theorem polynomial.splits_of_is_unit

deleted theorem polynomial.splits_of_map_degree_eq_one

deleted theorem polynomial.splits_of_map_eq_C

deleted theorem polynomial.splits_of_nat_degree_eq_one

deleted theorem polynomial.splits_of_nat_degree_le_one

deleted theorem polynomial.splits_of_splits_gcd_left

deleted theorem polynomial.splits_of_splits_gcd_right

deleted theorem polynomial.splits_of_splits_id

deleted theorem polynomial.splits_of_splits_mul'

deleted theorem polynomial.splits_of_splits_mul

deleted theorem polynomial.splits_of_splits_of_dvd

deleted theorem polynomial.splits_one

deleted theorem polynomial.splits_pow

deleted theorem polynomial.splits_prod

deleted theorem polynomial.splits_prod_iff

deleted theorem polynomial.splits_zero

deleted theorem polynomial.sum_roots_eq_next_coeff_of_monic_of_split

Created src/ring_theory/adjoin/field.lean

added def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly

added theorem finite_dimensional.of_subalgebra_to_submodule

added theorem lift_of_splits

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/vieta.lean

Modified src/topology/algebra/polynomial.lean