Commit 2022-02-17 19:35 aacc36c5

feat(group_theory/commensurable): Definition and lemmas about commensurability. (#9545) This defines commensurability for subgroups, proves this defines a transitive relation and then defines the commensurator subgroup. In doing so it also needs some lemmas about indices of subgroups and the definition of the conjugate of a subgroup by an element of the parent group.