Theorem IsScalarTower.coe_toAlgHom'

Modification history

2026-04-28 16:44
Mathlib/Algebra/Algebra/Hom.lean
chore(Algebra/Algebra/Tower): make `Algebra.algHom` an alias of `IsScalarTower.toAlgHom` (#38184) …
Modified IsScalarTower.coe_toAlgHom'View on Github →
2023-04-20 04:08
Mathlib/Algebra/Algebra/Tower.lean
chore: tidy various files (#3530)
Added IsScalarTower.coe_toAlgHom'View on Github →