Mathlib Changelog
v4
Changelog
About
Github
Theorem
AlgHomClass.toRingHom_toAlgHom
Modification history
2025-07-19 01:40
Mathlib/Algebra/Algebra/Hom.lean
feat: coercing to an `AlgHom` then `RingHom` (#27205) …
Added
AlgHomClass.toRingHom_toAlgHom
View on Github →