feat(group_theory/complement): The index of a complement of `H` equals the cardinality of `H` (#17250)
feat(group_theory/complement): The index of a complement of `H` equals the cardinality of `H` (#17250)

This PR adds a lemma stating that the index of a complement of `H` equals the cardinality of `H`.



Co-authored-by: Thomas Browning <25c750517795e47f172dc8c552ed72c7de260bd4@users.noreply.github.com>

leanprover-community/mathlib,leanprover-community/mathlib