Commit 2025-08-14 00:57 9a76f1a6

View on Github →

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

Rename IsAdjoinRoot.aequiv to IsAdjoinRoot.algEquiv (and associated lemmas)
Rename IsAdjoinRoot.ofEquiv to IsAdjoinRoot.ofAlgEquiv (and associated lemmas)
Correct a typo in the doc header

Estimated changes

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

deleted def IsAdjoinRoot.aequiv

deleted theorem IsAdjoinRoot.aequiv_aequiv

deleted theorem IsAdjoinRoot.aequiv_map

deleted theorem IsAdjoinRoot.aequiv_ofEquiv

deleted theorem IsAdjoinRoot.aequiv_root

deleted theorem IsAdjoinRoot.aequiv_self

deleted theorem IsAdjoinRoot.aequiv_symm

deleted theorem IsAdjoinRoot.aequiv_trans

added def IsAdjoinRoot.algEquiv

added theorem IsAdjoinRoot.algEquiv_algEquiv

added theorem IsAdjoinRoot.algEquiv_map

added theorem IsAdjoinRoot.algEquiv_ofAlgEquiv

added theorem IsAdjoinRoot.algEquiv_root

added theorem IsAdjoinRoot.algEquiv_self

added theorem IsAdjoinRoot.algEquiv_symm

added theorem IsAdjoinRoot.algEquiv_trans

deleted theorem IsAdjoinRoot.liftHom_aequiv

added theorem IsAdjoinRoot.liftHom_algEquiv

deleted theorem IsAdjoinRoot.lift_aequiv

added theorem IsAdjoinRoot.lift_algEquiv

added def IsAdjoinRoot.ofAlgEquiv

added theorem IsAdjoinRoot.ofAlgEquiv_algEquiv

added theorem IsAdjoinRoot.ofAlgEquiv_root

deleted def IsAdjoinRoot.ofEquiv

deleted theorem IsAdjoinRoot.ofEquiv_aequiv

deleted theorem IsAdjoinRoot.ofEquiv_root