Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 11:49 87b0084b

View on Github →

chore(field_theory/separable): generalize theorems (#10337)

Estimated changes

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.not_is_unit_X_sub_C

Modified src/data/polynomial/ring_division.lean

Modified src/field_theory/finite/basic.lean

Modified src/field_theory/primitive_element.lean

Modified src/field_theory/separable.lean

modified theorem irreducible.separable

modified theorem polynomial.coeff_contract

added theorem polynomial.contract_expand

modified theorem polynomial.count_roots_le_one

modified theorem polynomial.eq_X_sub_C_of_separable_of_root_eq

modified theorem polynomial.exists_separable_of_irreducible

modified theorem polynomial.expand_char

modified theorem polynomial.expand_contract

added theorem polynomial.expand_zero

modified theorem polynomial.is_unit_or_eq_zero_of_separable_expand

modified theorem polynomial.map_expand_pow_char

modified theorem polynomial.multiplicity_le_one_of_separable

modified theorem polynomial.nodup_of_separable_prod

modified theorem polynomial.nodup_roots

deleted theorem polynomial.not_unit_X_sub_C

modified theorem polynomial.of_irreducible_expand

modified theorem polynomial.of_irreducible_expand_pow

modified theorem polynomial.root_multiplicity_le_one_of_separable

modified theorem polynomial.separable.squarefree

modified theorem polynomial.separable_X_pow_sub_C_unit

added theorem polynomial.separable_of_subsingleton

deleted theorem polynomial.squarefree_X_pow_sub_C

modified theorem polynomial.unique_separable_of_irreducible

Modified src/field_theory/separable_degree.lean

Modified src/ring_theory/norm.lean

Modified src/ring_theory/polynomial/cyclotomic.lean

Modified src/ring_theory/roots_of_unity.lean

Modified src/ring_theory/trace.lean