Mathlib Changelog
v4
Changelog
About
Github
Def
MvPolynomial.toPolynomialAdjoinImageCompl
Modification history
2025-12-05 11:03
Mathlib/FieldTheory/SeparablyGenerated.lean
feat(FieldTheory): fg extension over perfect field is separably generated (#30998)
Added
MvPolynomial.toPolynomialAdjoinImageCompl
View on Github →