English
Schur–Zassenhaus: If a normal subgroup N has order coprime to its index, then there exists a right complement H with N.IsComplement' H.
Русский
Лемма Шура-Цассенауска: если нормальная подгруппа N имеет порядок, взаимно простой с индексом, то существует правая комплемента N.
LaTeX
$$∀ {N : Subgroup G} [N.Normal], Nat.Coprime (Nat.card N) N.index → ∃ H : Subgroup G, IsComplement' N H$$
Lean4
/-- The quotient of the transversals of an abelian normal `N` by the `diff` relation. -/
def QuotientDiff :=
Quotient
(Setoid.mk (fun α β => diff (MonoidHom.id H) α β = 1)
⟨fun α => diff_self (MonoidHom.id H) α, fun h => by rw [← diff_inv, h, inv_one], fun h h' => by
rw [← diff_mul_diff, h, h', one_mul]⟩)
