Commit 2023-06-15 07:21 bbc68ef0

View on Github →

feat: port FieldTheory.SplittingField.Construction (#4891)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

Created Mathlib/FieldTheory/SplittingField/Construction.lean

added def Polynomial.IsSplittingField.algEquiv

added theorem Polynomial.SplittingField.adjoin_rootSet

added theorem Polynomial.SplittingField.adjoin_roots

added def Polynomial.SplittingField.algEquivSplittingFieldAux

added def Polynomial.SplittingField.lift

added def Polynomial.SplittingField

added theorem Polynomial.SplittingFieldAux.adjoin_rootSet

added def Polynomial.SplittingFieldAux.algEquivQuotientMvPolynomial

added theorem Polynomial.SplittingFieldAux.algebraMap_succ

added def Polynomial.SplittingFieldAux.ofMvPolynomial

added theorem Polynomial.SplittingFieldAux.ofMvPolynomial_surjective

added theorem Polynomial.SplittingFieldAux.succ

added def Polynomial.SplittingFieldAux

added def Polynomial.SplittingFieldAuxAux

added theorem Polynomial.X_sub_C_mul_removeFactor

added theorem Polynomial.fact_irreducible_factor

added def Polynomial.factor

added theorem Polynomial.factor_dvd_of_degree_ne_zero

added theorem Polynomial.factor_dvd_of_natDegree_ne_zero

added theorem Polynomial.factor_dvd_of_not_isUnit

added theorem Polynomial.irreducible_factor

added theorem Polynomial.natDegree_removeFactor'

added theorem Polynomial.natDegree_removeFactor

added def Polynomial.removeFactor