Def IsAdjoinRoot.ofEquiv

Modification history

2025-08-14 00:57

Mathlib/RingTheory/IsAdjoinRoot.lean

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

Deleted IsAdjoinRoot.ofEquiv View on Github →

2025-07-23 19:36

Mathlib/RingTheory/IsAdjoinRoot.lean

style(RingTheory/IsAdjoinRoot): improve style and golf (#27374) …

Modified IsAdjoinRoot.ofEquiv View on Github →

2023-06-19 04:18

Mathlib/RingTheory/IsAdjoinRoot.lean

feat: port RingTheory.IsAdjoinRoot (#5190)

Added IsAdjoinRoot.ofEquiv View on Github →