mathlib3

aacc36c5 - feat(group_theory/commensurable): Definition and lemmas about commensurability. (#9545)

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. Co-authored-by: CBirkbeck <56166236+CBirkbeck@users.noreply.github.com>