Commit 2023-06-23 10:52 d74c7389

View on Github →

feat: port FieldTheory.PolynomialGaloisGroup (#5159)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/PolynomialGaloisGroup.lean

added theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv

added theorem Polynomial.Gal.card_of_separable

added theorem Polynomial.Gal.ext

added def Polynomial.Gal.galActionHom

added theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree'

added theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree

added theorem Polynomial.Gal.galActionHom_injective

added theorem Polynomial.Gal.galActionHom_restrict

added def Polynomial.Gal.mapRoots

added theorem Polynomial.Gal.mapRoots_bijective

added theorem Polynomial.Gal.mul_splits_in_splittingField_of_mul

added theorem Polynomial.Gal.prime_degree_dvd_card

added def Polynomial.Gal.restrict

added def Polynomial.Gal.restrictComp

added theorem Polynomial.Gal.restrictComp_surjective

added def Polynomial.Gal.restrictDvd

added theorem Polynomial.Gal.restrictDvd_def

added theorem Polynomial.Gal.restrictDvd_surjective

added def Polynomial.Gal.restrictProd

added theorem Polynomial.Gal.restrictProd_injective

added theorem Polynomial.Gal.restrict_smul

added theorem Polynomial.Gal.restrict_surjective

added def Polynomial.Gal.rootsEquivRoots

added theorem Polynomial.Gal.smul_def

added theorem Polynomial.Gal.splits_in_splittingField_of_comp

added theorem Polynomial.Gal.splits_ℚ_ℂ

added def Polynomial.Gal.uniqueGalOfSplits

added def Polynomial.Gal

Modified Mathlib/FieldTheory/SplittingField/Construction.lean