Mathlib Changelog
v4
Changelog
About
Github
Theorem
AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom
Modification history
2025-07-21 19:28
Mathlib/RingTheory/Adjoin/Field.lean
feat: API for `Minpoly.toAdjoin` and friends (#27278) …
Added
AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom
View on Github →