# The Schur-Zassenhaus Theorem #

In this file we prove the Schur-Zassenhaus theorem.

## Main results #

`exists_right_complement'_of_coprime`

: The**Schur-Zassenhaus**theorem: If`H : Subgroup G`

is normal and has order coprime to its index, then there exists a subgroup`K`

which is a (right) complement of`H`

.`exists_left_complement'_of_coprime`

: The**Schur-Zassenhaus**theorem: If`H : Subgroup G`

is normal and has order coprime to its index, then there exists a subgroup`K`

which is a (left) complement of`H`

.

The quotient of the transversals of an abelian normal `N`

by the `diff`

relation.

## Equations

- H.QuotientDiff = Quotient { r := fun (α β : ↑(Subgroup.leftTransversals ↑H)) => Subgroup.leftTransversals.diff (MonoidHom.id ↥H) α β = 1, iseqv := ⋯ }

## Instances For

## Equations

- Subgroup.instMulActionQuotientDiff = MulAction.mk ⋯ ⋯

## Proof of the Schur-Zassenhaus theorem #

In this section, we prove the Schur-Zassenhaus theorem.
The proof is by contradiction. We assume that `G`

is a minimal counterexample to the theorem.

We will arrive at a contradiction via the following steps:

- step 0:
`N`

(the normal Hall subgroup) is nontrivial. - step 1: If
`K`

is a subgroup of`G`

with`K ⊔ N = ⊤`

, then`K = ⊤`

. - step 2:
`N`

is a minimal normal subgroup, phrased in terms of subgroups of`G`

. - step 3:
`N`

is a minimal normal subgroup, phrased in terms of subgroups of`N`

. - step 4:
`p`

(`min_fact (Fintype.card N)`

) is prime (follows from step0). - step 5:
`P`

(a Sylow`p`

-subgroup of`N`

) is nontrivial. - step 6:
`N`

is a`p`

-group (applies step 1 to the normalizer of`P`

in`G`

). - step 7:
`N`

is abelian (applies step 3 to the center of`N`

).

Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`

**Schur-Zassenhaus** for normal subgroups:
If `H : Subgroup G`

is normal, and has order coprime to its index, then there exists a
subgroup `K`

which is a (right) complement of `H`

.

**Schur-Zassenhaus** for normal subgroups:
If `H : Subgroup G`

is normal, and has order coprime to its index, then there exists a
subgroup `K`

which is a (left) complement of `H`

.