instMul

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#NatOrdinal.instMul

English

Natural multiplication is commutative: a ⨳ b = b ⨳ a.

Русский

Натуральное умножение коммутативно: a ⨳ b = b ⨳ a.

LaTeX

$$$\\forall a,b \\in \\mathrm{Ordinal},\\ a \\nabla b = b \\nabla a$$$

Lean4

instance : Mul NatOrdinal :=
  ⟨nmul⟩

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

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

Разделы

Аффилиация

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