mathlib

0fd99294 - feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490)

feat(group_theory/double_cosets): definition of double cosets and some basic lemmas. (#9490) This contains the definition of double cosets and some basic lemmas about them, such as "the whole group is the disjoint union of its double cosets" and relationship to usual group quotients.