card_mul_card — Mathlib

English

If S and T form a complement of G (finite case), then the product of their cardinalities equals the cardinality of G: |S| · |T| = |G|.

Русский

Если S и T образуют дополнение к G (в конечном случае), тогда произведение их кардинальностей равно кардинальности G: |S| · |T| = |G|.

LaTeX

$$$|S| \\cdot |T| = |G|$$

Lean4

@[to_additive AddSubgroup.IsComplement.card_mul_card]
theorem card_mul_card (h : IsComplement S T) : Nat.card S * Nat.card T = Nat.card G :=
  (Nat.card_prod _ _).symm.trans <| Nat.card_congr <| Equiv.ofBijective _ h

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