Def IsScalarTower.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.toAlgHom View on Github →

2023-03-01 10:14

Mathlib/Algebra/Algebra/Tower.lean

feat: Port Algebra.Algebra.Tower (#2548)

Added IsScalarTower.toAlgHom View on Github →