mathlib

3d6291ea - chore(algebra/group/with_one): Use bundled morphisms (#4957)

chore(algebra/group/with_one): Use bundled morphisms (#4957) The comment "We have no bundled semigroup homomorphisms" has become false, these exist as `mul_hom`. This also adds `with_one.coe_mul_hom` and `with_zero.coe_add_hom`