card_prod — Mathlib

English

The cardinality of the Cartesian product equals the product of the cardinalities: |α × β| = |α| · |β|.

Русский

Кардинал декартова произведения равен произведению кардиналов: |α × β| = |α| · |β|.

LaTeX

$$$|\\alpha \\times \\beta| = |\\alpha| \\cdot |\\beta|$$$

Lean4

@[simp]
theorem card_prod (α β : Type*) [Fintype α] [Fintype β] : Fintype.card (α × β) = Fintype.card α * Fintype.card β :=
  card_product _ _

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