mathlib

eb22ba4f - chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses (#13389)

chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses (#13389) This replaces `mul_hom` with `mul_hom_class` and `add_hom` with `add_hom_class`. Also adds two trivial lemmas, `monoid_algebra.map_domain_one` and `add_monoid_algebra.map_domain_one`.