Commit 2026-09-22 13:54 8d7d0c46

View on Github →

chore(Algebra): coe_ringHom -> coe_toRingHom (#38966)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

deleted theorem AlgEquiv.coe_ringEquiv

deleted theorem AlgEquiv.coe_ringEquiv_injective

deleted theorem AlgEquiv.coe_ringHom_commutes

added theorem AlgEquiv.coe_toRingEquiv

added theorem AlgEquiv.toRingEquiv_injective

added theorem AlgEquiv.toRingHom_toAlgHom

Modified Mathlib/Algebra/Algebra/Hom.lean

deleted theorem AlgHom.coe_ringHom_injective

deleted theorem AlgHom.coe_ringHom_mk

added theorem AlgHom.toRingHom_injective

added theorem AlgHom.toRingHom_mk

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

deleted theorem MvPolynomial.mapAlgHom_coe_ringHom

added theorem MvPolynomial.toRingHom_mapAlgHom

Modified Mathlib/Algebra/Order/Hom/Ring.lean

deleted theorem OrderRingHom.coe_coe_ringHom

deleted theorem OrderRingHom.coe_ringHom_apply

deleted theorem OrderRingHom.coe_ringHom_id

added theorem OrderRingHom.coe_toRingHom

added theorem OrderRingHom.toRingHom_apply

added theorem OrderRingHom.toRingHom_id

deleted theorem OrderRingIso.coe_ringEquiv_refl

added theorem OrderRingIso.toRingEquiv_refl

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

deleted theorem Polynomial.mapAlgEquiv_coe_ringHom

deleted theorem Polynomial.mapAlgHom_coe_ringHom

added theorem Polynomial.toRingHom_mapAlgEquiv

added theorem Polynomial.toRingHom_mapAlgHom

Modified Mathlib/Algebra/Ring/Equiv.lean

deleted theorem RingEquiv.coe_ringHom_inj_iff

deleted theorem RingEquiv.coe_ringHom_ofRingHom

deleted theorem RingEquiv.coe_ringHom_refl

deleted theorem RingEquiv.coe_ringHom_trans

deleted theorem RingEquiv.ofRingHom_coe_ringHom

added theorem RingEquiv.ofRingHom_toRingHom

added theorem RingEquiv.toRingHom_inj_iff

added theorem RingEquiv.toRingHom_ofRingHom

added theorem RingEquiv.toRingHom_refl'

modified theorem RingEquiv.toRingHom_refl

added theorem RingEquiv.toRingHom_trans'

modified theorem RingEquiv.toRingHom_trans

Modified Mathlib/AlgebraicGeometry/Group/Affine.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/UniversallyInjective.lean

Modified Mathlib/AlgebraicGeometry/Spec.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/FieldTheory/Extension.lean

Modified Mathlib/FieldTheory/IsAlgClosed/Basic.lean

Modified Mathlib/FieldTheory/PurelyInseparable/Basic.lean

Modified Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean

Modified Mathlib/NumberTheory/NumberField/CMField.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/DedekindDomain/Instances.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

Modified Mathlib/RingTheory/FractionalIdeal/Operations.lean

Modified Mathlib/RingTheory/GradedAlgebra/AlgHom.lean

Modified Mathlib/RingTheory/GradedAlgebra/RingHom.lean

deleted theorem GradedRingHom.coe_ringHom_injective

added theorem GradedRingHom.toRingHom_injective

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/FractionRing.lean

Modified Mathlib/RingTheory/RingHom/StandardSmooth.lean

Modified Mathlib/RingTheory/RingInvo.lean

deleted theorem RingInvo.coe_ringEquiv

added theorem RingInvo.toRingEquiv_apply

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/RingTheory/Unramified/Basic.lean