Commit 2025-10-12 13:56 cb38ed14

View on Github →

refactor(RingTheory/AdjoinRoot): generalise algEquivOfAssociated (#30456) Generalise algEquivOfAssociated from fields to commutative rings, and use it to define algEquivOfEq. Also make the f and g arguments explicit to avoid there only being Prop arguments to the defs.

Estimated changes

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

deleted theorem AdjoinRoot.algEquivOfAssociated_apply_root

deleted theorem AdjoinRoot.algEquivOfAssociated_toAlgHom

deleted theorem AdjoinRoot.algHomOfDvd_apply_root

deleted theorem AdjoinRoot.coe_algEquivOfAssociated

deleted theorem AdjoinRoot.coe_algHomOfDvd

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.algEquivOfAssociated_root

added theorem AdjoinRoot.algEquivOfAssociated_symm

added theorem AdjoinRoot.algEquivOfAssociated_toAlgHom

deleted def AdjoinRoot.algEquivOfEq

modified theorem AdjoinRoot.algEquivOfEq_root

modified theorem AdjoinRoot.algEquivOfEq_symm

added theorem AdjoinRoot.algEquivOfEq_toAlgHom

added theorem AdjoinRoot.algHomOfDvd_root

added theorem AdjoinRoot.coe_algEquivOfAssociated

added theorem AdjoinRoot.coe_algEquivOfEq

added theorem AdjoinRoot.coe_algHomOfDvd