card_mul

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.card_mul

English

Cardinal of product equals product of cardinals: card(a*b) = card(a) card(b).

Русский

Кардинал произведения равен произведению кардиналов: card(a·b) = card(a) card(b).

LaTeX

$$card(a*b) = card(a) * card(b)$$

Lean4

@[simp]
theorem card_mul (a b) : card (a * b) = card a * card b :=
  Quotient.inductionOn₂ a b fun ⟨α, _r, _⟩ ⟨β, _s, _⟩ => mul_comm #β #α

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru