isComplement'_of_coprime — Mathlib

English

If H and K are subgroups of finite G with |H| · |K| = |G| and gcd(|H|, |K|) = 1, then H and K form a complement in G.

Русский

Если H и K — подгруппы конечной G, и |H| · |K| = |G|, а gcd(|H|, |K|) = 1, то H и K образуют дополнение в G.

LaTeX

$$[Finite G] ∧ (|H| · |K| = |G|) ∧ Nat.Coprime(|H|,|K|) ⇒ IsComplement'(H,K)$$

Lean4

theorem isComplement'_of_coprime [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G)
    (h2 : Nat.Coprime (Nat.card H) (Nat.card K)) : IsComplement' H K :=
  isComplement'_of_card_mul_and_disjoint h1 (disjoint_iff.mpr (inf_eq_bot_of_coprime h2))

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