card_prod — Mathlib

English

If α and β are finite, then Nat.card (α × β) = Nat.card α · Nat.card β.

Русский

Если α и β конечны, то кардинальность произведения α × β равна произведению кардинальностей α и β.

LaTeX

$$$$ Nat.card(\alpha \times \beta) = Nat.card(\alpha) \cdot Nat.card(\beta) $$$$

Lean4

@[simp]
theorem card_prod (α β : Type*) : Nat.card (α × β) = Nat.card α * Nat.card β := by
  simp only [Nat.card, mk_prod, toNat_mul, toNat_lift]

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