Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-12 19:52 9fb89647

View on Github →

refactor(field_theory/splitting_field/is_splitting_field): use root_set (#19179)

Estimated changes

Modified src/field_theory/finite/galois_field.lean

Modified src/field_theory/galois.lean

Modified src/field_theory/normal.lean

Modified src/field_theory/polynomial_galois_group.lean

Modified src/field_theory/splitting_field/construction.lean

modified theorem polynomial.splitting_field.adjoin_root_set

deleted theorem polynomial.splitting_field.adjoin_roots

added theorem polynomial.splitting_field_aux.adjoin_root_set

deleted theorem polynomial.splitting_field_aux.adjoin_roots

Modified src/field_theory/splitting_field/is_splitting_field.lean

Modified src/number_theory/cyclotomic/basic.lean

modified theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots

modified theorem is_cyclotomic_extension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic