Def IsAdjoinRootMonic.mkOfAdjoinEqTop'

Modification history

2026-07-01 08:33
Mathlib/RingTheory/IsAdjoinRoot.lean
feat: simplify proof of `IsAdjoinRootMonic.mkOfAdjoinEqTop'` (#38189) …
Modified IsAdjoinRootMonic.mkOfAdjoinEqTop'View on Github →
2026-04-15 19:09
Mathlib/RingTheory/IsAdjoinRoot.lean
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) …
Added IsAdjoinRootMonic.mkOfAdjoinEqTop'View on Github →