mathlib3

c2e9ec02 - feat(group_theory/subgroup): add {monoid,add_monoid,ring}_hom.lift_of_right_inverse (#6814)