Commit 2021-10-01 06:05 57fa903f

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.