mathlib3

3256cf69 - 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 <tb65536@users.noreply.github.com>