Commit 2026-06-24 18:12 2929a789

View on Github →

chore(Algebra): coe_algHom -> coe_toAlgHom (#38950)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

deleted theorem AlgEquiv.coe_algHom

deleted theorem AlgEquiv.coe_algHom_injective

deleted theorem AlgEquiv.coe_algHom_ofAlgHom

added theorem AlgEquiv.coe_toAlgHom

added theorem AlgEquiv.coe_toAlgHom_injective

deleted theorem AlgEquiv.ofAlgHom_coe_algHom

added theorem AlgEquiv.ofAlgHom_toAlgHom

added theorem AlgEquiv.toAlgHom_ofAlgHom

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Centralizer.lean

Modified Mathlib/Algebra/Azumaya/Basic.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/AlgebraicGeometry/AffineSpace.lean

Modified Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Modified Mathlib/FieldTheory/Extension.lean

Modified Mathlib/FieldTheory/Galois/Basic.lean

Modified Mathlib/FieldTheory/Isaacs.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/LinearDisjoint.lean

Modified Mathlib/FieldTheory/Minpoly/Field.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/FieldTheory/SeparablyGenerated.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean

Modified Mathlib/NumberTheory/Cyclotomic/Gal.lean

Modified Mathlib/RingTheory/Algebraic/MvPolynomial.lean

Modified Mathlib/RingTheory/Bialgebra/Equiv.lean

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

deleted theorem BialgHom.coe_algHom_injective

added theorem BialgHom.coe_toAlgHom_injective

Modified Mathlib/RingTheory/DividedPowerAlgebra/Init.lean

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

Modified Mathlib/RingTheory/Extension/Presentation/Core.lean

Modified Mathlib/RingTheory/GradedAlgebra/AlgHom.lean

deleted theorem GradedAlgHom.coe_algHom_injective

deleted theorem GradedAlgHom.coe_algHom_mk

added theorem GradedAlgHom.coe_toAlgHom_injective

added theorem GradedAlgHom.coe_toAlgHom_mk

deleted theorem GradedAlgHom.restrictScalars_coe_algHom

added theorem GradedAlgHom.restrictScalars_toAlgHom

Modified Mathlib/RingTheory/GradedAlgebra/TensorProduct.lean

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Modified Mathlib/RingTheory/NoetherNormalization.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Factorization.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/RingTheory/Smooth/IntegralClosure.lean

Modified Mathlib/RingTheory/TensorProduct/Maps.lean