mathlib3

92a5be8d - feat(ring,group,monoid): map_equiv lemmas for different structures (#8453)

feat(ring,group,monoid): map_equiv lemmas for different structures (#8453) There is some inconsistency in the statements of these lemmas because there is a coercion from `ring_equiv` to `ring_hom`, but not `mul_equiv` to `monoid_hom`. Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>