mathlib3

57fa903f - refactor(group_theory/complement): Split `complement.lean` (#9474)

refactor(group_theory/complement): Split `complement.lean` (#9474) Splits off Schur-Zassenhaus from `complement.lean`. In the new file, we can replace `fintype.card (quotient_group.quotient H)` with `H.index`. Advantages: We can avoid importing `cardinal.lean` in `complement.lean`. Later (once full SZ is proved), we can avoid importing `sylow.lean` in `complement.lean`.