mathlib

4f757600 - chore(*/hom,equiv): Split `monoid_hom` into more fundamental structures, and reuse them elsewhere (#4423)

chore(*/hom,equiv): Split `monoid_hom` into more fundamental structures, and reuse them elsewhere (#4423) Notably this adds `add_hom` and `mul_hom`, which become base classes of `add_equiv`, `mul_equiv`, `linear_map`, and `linear_equiv`. Primarily to avoid breaking assumptions of field order in `monoid_hom` and `add_monoid_hom`, this also adds `one_hom` and `zero_hom`. A massive number of lemmas here are totally uninteresting and hold for pretty much all objects that define `coe_to_fun`. This PR translates all those lemmas, but doesn't bother attempting to generalize later ones.