Theorem IsAdjoinRoot.ofAlgEquiv_root

Modification history

2025-08-18 12:21

Mathlib/RingTheory/IsAdjoinRoot.lean

feat(RingTheory/IsAdjoinRoot): add properties and constructors (#27373) …

Modified IsAdjoinRoot.ofAlgEquiv_root View on Github →

2025-08-14 00:57

Mathlib/RingTheory/IsAdjoinRoot.lean

chore(RingTheory/IsAdjoinRoot): rename operations (#28293) …

Added IsAdjoinRoot.ofAlgEquiv_root View on Github →