Commit 2024-01-09 20:44 0470fa9f
View on Github →feat: MonoidHom is equivalent to MulAction + IsScalarTower (#9381)
Natural strengthening/extension of MonoidHom/RingHom.smulOneHom. Follow-up of #9064.
monoidHomEquivMulActionIsScalarTower: A homomorphism between two monoids M and N can be equivalently specified by a multiplicative action of M on N that is compatible with the multiplication on N.
ringHomEquivModuleIsScalarTower: A homomorphism between semirings R and S can be equivalently specified by a R-module structure on S such that S/S/R is a scalar tower.
Mathlib doesn't have a typeclass for RingHom between noncommutative rings, but ringHomEquivModuleIsScalarTower shows we can achieve the same effect with the combination of Module + IsScalarTower.