isComplement'_of_card_mul_and_disjoint

English

If G is finite and |H| · |K| = |G| with H ∩ K = {e}, then H and K form a complement in G.

Русский

Если G конечна и |H| · |K| = |G| и H ∩ K = {e}, то H и K образуют дополнение в G.

LaTeX

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

Lean4

theorem isComplement'_of_card_mul_and_disjoint [Finite G] (h1 : Nat.card H * Nat.card K = Nat.card G)
    (h2 : Disjoint H K) : IsComplement' H K :=
  (Nat.bijective_iff_injective_and_card _).mpr ⟨mul_injective_of_disjoint h2, (Nat.card_prod H K).trans h1⟩

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