Commit 2026-04-28 16:44 66555f3d

View on Github →

chore(Algebra/Algebra/Tower): make Algebra.algHom an alias of IsScalarTower.toAlgHom (#38184) Algebra.algHom is a duplicate of IsScalarTower.ofAlgHom so I've made it an alias to make this clearer. Zulip thread: #mathlib4 > duplication: Algebra.algHom = IsScalarTower.toAlgHom

Estimated changes