mathlib3

8a0d5e07 - feat(group_theory/complement): define subgroup complement, prove Schur-Zassenhaus (#8008)

feat(group_theory/complement): define subgroup complement, prove Schur-Zassenhaus (#8008) Defines complements, and proves Schur-Zassenhaus for abelian normal subgroups. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>