mathlib3

468328da - chore(group_theory/subgroup): the range of a monoid/group/ring/module hom from a finite type is finite (#8293)

chore(group_theory/subgroup): the range of a monoid/group/ring/module hom from a finite type is finite (#8293) We have this fact for maps of types, but when changing `is_group_hom` etc from classes to structures one needs it for other bundled maps. The proofs use the power of the `copy` trick.