Commit 2020-10-08 05:32 4f757600

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.