Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-08-23 07:42
8283eb95
View on Github →
chore: simplify construction of splitting field (
#6735
)
Estimated changes
Modified
Mathlib/FieldTheory/SplittingField/Construction.lean
deleted
def
Polynomial.SplittingFieldAux.algEquivQuotientMvPolynomial
deleted
def
Polynomial.SplittingFieldAux.ofMvPolynomial
deleted
theorem
Polynomial.SplittingFieldAux.ofMvPolynomial_surjective