Commit 2023-06-06 05:32 c6a63ba1

View on Github →

feat: port FieldTheory.SplittingField.IsSplittingField (#4714)

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

added theorem IntermediateField.splits_of_splits

added theorem Polynomial.IsSplittingField.adjoin_roots

added theorem Polynomial.IsSplittingField.finiteDimensional

added def Polynomial.IsSplittingField.lift

added theorem Polynomial.IsSplittingField.mul

added theorem Polynomial.IsSplittingField.of_algEquiv

added theorem Polynomial.IsSplittingField.splits

added theorem Polynomial.IsSplittingField.splits_iff