Commit 2025-10-10 05:35 4a3989c2

View on Github →

chore(RingTheory/AdjoinRoot): move AdjoinRoot.algEquivOfEq earlier (#30300) Before this PR it was in Mathlib.FieldTheory.IntermediateField.Adjoin.Basic and required Field K. This PR moves it to Mathlib.RingTheory.AdjoinRoot and replaces the Field assumption by CommRing while simplifying the proof.

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

deleted theorem AdjoinRoot.algEquivOfEq_apply_root

deleted theorem AdjoinRoot.algEquivOfEq_toAlgHom

deleted theorem AdjoinRoot.coe_algEquivOfEq

Modified Mathlib/RingTheory/AdjoinRoot.lean

modified theorem AdjoinRoot.aeval_eq

added theorem AdjoinRoot.aeval_eq_of_algebra

added def AdjoinRoot.algEquivOfEq

added theorem AdjoinRoot.algEquivOfEq_root

added theorem AdjoinRoot.algEquivOfEq_symm