feat(group_theory/complement): The range of a section `G ⧸ H → G` is a transversal (#13623)
feat(group_theory/complement): The range of a section `G ⧸ H → G` is a transversal (#13623)

This PR adds left and right versions of the statement that the range of a section `G ⧸ H → G` is a transversal.





leanprover-community/mathlib,leanprover-community/mathlib