Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-23 19:49 9893a260

View on Github →

chore(field_theory/splitting_field): module doc and generalise one lemma (#6739) This PR provides a module doc for field_theory.splitting_field, which is the last file without module doc in field_theory. Furthermore, I took the opportunity of renaming the fields in that file from \alpha, \beta, \gamma to K, L, F to make it more readable for newcomers. Moved nat_degree_multiset_prod, to algebra.polynomial.big_operators). In order to get the no_zero_divisors instance on polynomial R, I had to include data.polynomial.ring_division in that file. Furthermore, with the help of Damiano, generalised this lemma to no_zero_divisors R. Coauthored by: Damiano Testa adomani@gmail.com

Estimated changes

Modified src/algebra/polynomial/big_operators.lean

added theorem polynomial.nat_degree_multiset_prod

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/splitting_field.lean

modified theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C

modified theorem polynomial.X_sub_C_mul_remove_factor

modified theorem polynomial.degree_eq_card_roots

modified theorem polynomial.degree_eq_one_of_irreducible_of_splits

modified theorem polynomial.eq_X_sub_C_of_splits_of_single_root

modified theorem polynomial.eq_prod_roots_of_splits

modified theorem polynomial.exists_multiset_of_splits

modified theorem polynomial.exists_root_of_splits

modified def polynomial.factor

modified theorem polynomial.factor_dvd_of_degree_ne_zero

modified theorem polynomial.factor_dvd_of_nat_degree_ne_zero

modified theorem polynomial.factor_dvd_of_not_is_unit

modified def polynomial.is_splitting_field.alg_equiv

modified theorem polynomial.is_splitting_field.finite_dimensional

modified def polynomial.is_splitting_field.lift

modified theorem polynomial.is_splitting_field.mul

modified theorem polynomial.is_splitting_field.splits_iff

modified theorem polynomial.map_root_of_splits

modified theorem polynomial.nat_degree_eq_card_roots

deleted theorem polynomial.nat_degree_multiset_prod

modified theorem polynomial.nat_degree_remove_factor'

modified theorem polynomial.nat_degree_remove_factor

modified theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq

modified def polynomial.remove_factor

modified def polynomial.root_of_splits

modified theorem polynomial.roots_map

modified def polynomial.splits

modified theorem polynomial.splits_C

modified theorem polynomial.splits_X_sub_C

modified theorem polynomial.splits_comp_of_splits

modified theorem polynomial.splits_id_iff_splits

modified theorem polynomial.splits_iff_card_roots

modified theorem polynomial.splits_iff_exists_multiset

modified theorem polynomial.splits_map_iff

modified theorem polynomial.splits_mul

modified theorem polynomial.splits_mul_iff

modified theorem polynomial.splits_of_degree_eq_one

modified theorem polynomial.splits_of_degree_le_one

modified theorem polynomial.splits_of_exists_multiset

modified theorem polynomial.splits_of_is_unit

modified theorem polynomial.splits_of_nat_degree_eq_one

modified theorem polynomial.splits_of_nat_degree_le_one

modified theorem polynomial.splits_of_splits_gcd_left

modified theorem polynomial.splits_of_splits_gcd_right

modified theorem polynomial.splits_of_splits_id

modified theorem polynomial.splits_of_splits_mul

modified theorem polynomial.splits_of_splits_of_dvd

modified theorem polynomial.splits_pow

modified theorem polynomial.splits_prod

modified theorem polynomial.splits_prod_iff

modified theorem polynomial.splits_zero

modified theorem polynomial.splitting_field.adjoin_root_set

modified theorem polynomial.splitting_field.adjoin_roots

modified def polynomial.splitting_field.lift

modified def polynomial.splitting_field

modified theorem polynomial.splitting_field_aux.adjoin_roots

modified theorem polynomial.splitting_field_aux.algebra_map_succ

modified theorem polynomial.splitting_field_aux.exists_lift

modified theorem polynomial.splitting_field_aux.succ

modified def polynomial.splitting_field_aux