Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-20 10:07 19290257

View on Github →

feat(ring_theory/polynomial/cyclotomic): generalize a few results to domains (#10741) Primarily for flt-regular

Estimated changes

Modified src/data/multiset/basic.lean

Modified src/data/polynomial/degree/definitions.lean

modified theorem polynomial.degree_X_add_C

Modified src/data/polynomial/field_division.lean

modified theorem polynomial.prod_multiset_root_eq_finset_root

modified theorem polynomial.roots_C_mul

modified theorem polynomial.roots_normalize

Modified src/field_theory/splitting_field.lean

deleted theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C_of_field

deleted theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field

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

modified theorem polynomial.X_pow_sub_one_eq_prod

modified theorem polynomial.cyclotomic'_eq_X_pow_sub_one_div

modified theorem polynomial.cyclotomic_eq_prod_X_sub_primitive_roots

modified theorem polynomial.int_coeff_of_cyclotomic'

modified theorem polynomial.prod_cyclotomic'_eq_X_pow_sub_one

modified theorem polynomial.unique_int_coeff_of_cycl

Modified src/ring_theory/roots_of_unity.lean