mathlib

b1b2cab4 - 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.