mathlib3

a3997288 - feat(group_theory/coset): Interaction between quotient_group.mk and right multiplication by elements of the subgroup (#8970)

feat(group_theory/coset): Interaction between quotient_group.mk and right multiplication by elements of the subgroup (#8970) Two helpful lemmas regarding the interaction between `quotient_group.mk` and right multiplication by elements of the subgroup. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>