nmul_eq_mul — Mathlib

English

For any ordinals a,b, the natural product a ⊗ b equals the ordinal obtained by applying toNatOrdinal to a and b, multiplying, and embedding back: a ⊗ b = toOrdinal(toNatOrdinal(a) · toNatOrdinal(b)).

Русский

Для любых ординалов a,b естественное произведение равно образу обычного произведения через вложение: a ⊗ b = toOrdinal(toNatOrdinal(a) · toNatOrdinal(b)).

LaTeX

$$$a \otimes b = \operatorname{toOrdinal}(\operatorname{toNatOrdinal}(a) \cdot \operatorname{toNatOrdinal}(b))$$$

Lean4

theorem nmul_eq_mul (a b) : a ⨳ b = toOrdinal (toNatOrdinal a * toNatOrdinal b) :=
  rfl

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