PR #9490: feat(group_theory/double_cosets): definition of...

Stream: triage

[Random Issue Bot]

Today I chose PR 9490 for discussion!

feat(group_theory/double_cosets): definition of double cosets and some basic lemmas.
Created by @Chris Birkbeck (@CBirkbeck) on 2021-10-01
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?