Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-15 06:31 e3f4be1f

View on Github →

chore(field_theory/splitting_field): refactor splitting_field (#19178) We refactor the definition of splitting_field. The main motivation is to backport [!4#4891](https://github.com/leanprover-community/mathlib4/pull/4891) since the is seems very problematic to port the current design. Zulip discussion relevant to this PR: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234891.20.20FieldTheory.2ESplittingField

Estimated changes

Modified src/field_theory/abel_ruffini.lean

Modified src/field_theory/finite/galois_field.lean

Modified src/field_theory/polynomial_galois_group.lean

Modified src/field_theory/splitting_field/construction.lean

added def polynomial.splitting_field.alg_equiv_splitting_field_aux

added def polynomial.splitting_field_aux.alg_equiv_quotient_mv_polynomial

deleted theorem polynomial.splitting_field_aux.exists_lift

added def polynomial.splitting_field_aux.of_mv_polynomial

added theorem polynomial.splitting_field_aux.of_mv_polynomial_surjective

modified def polynomial.splitting_field_aux

added def polynomial.splitting_field_aux_aux

Modified src/number_theory/cyclotomic/basic.lean

Modified src/number_theory/cyclotomic/gal.lean

Modified src/number_theory/legendre_symbol/add_character.lean

added theorem add_char.primitive_add_char.prim

added def add_char.primitive_add_char

deleted structure add_char.primitive_add_char

Modified src/number_theory/legendre_symbol/gauss_sum.lean

Modified src/ring_theory/polynomial/gauss_lemma.lean