exists_left_complement'_of_coprime

English

If N is normal and coprime with its index, there exists a left complement H.

Русский

Если нормальная подгруппа N имеет порядок, взаимно простой с индексом, существует левый комплемент H.

LaTeX

$$∃ H : Subgroup G, IsComplement' H N$$

Lean4

/-- **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`. -/
theorem exists_left_complement'_of_coprime {N : Subgroup G} [N.Normal] (hN : Nat.Coprime (Nat.card N) N.index) :
    ∃ H : Subgroup G, IsComplement' H N :=
  Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime hN)

Похожие утверждения