Commit 2025-07-19 01:40 17ef2187

View on Github →

feat: coercing to an AlgHom then RingHom (#27205) From Toric

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem AlgHomClass.toRingHom_toAlgHom

Modified Mathlib/Topology/Algebra/Algebra.lean

modified theorem Subalgebra.coe_valA