Theorem IsAdjoinRootMonic.mkOfAdjoinEqTop'_root

Modification history

2026-04-15 19:09
Mathlib/RingTheory/IsAdjoinRoot.lean
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) …
Added IsAdjoinRootMonic.mkOfAdjoinEqTop'_rootView on Github →