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