card_mul — Mathlib

English

If H and K are complementary subgroups of G (HK = G and H ∩ K = {e}), then the product of their orders equals the order of G: |H| · |K| = |G|.

Русский

Если H и K — взаимодополняющие подгруппы G (HK = G и H ∩ K = {e}), то произведение их порядков равно порядку G: |H| · |K| = |G|.

LaTeX

$$IsComplement'(H,K) \Rightarrow |H| \cdot |K| = |G|$$

Lean4

theorem card_mul (h : IsComplement' H K) : Nat.card H * Nat.card K = Nat.card G :=
  IsComplement.card_mul h

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