noZeroDivisors

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

Continuation of left distributivity for ordinal multiplication.

Русский

Продолжение левого распределения для умножения ординалов.

LaTeX

$$LeftDistribClass(Ordinal)$$

Lean4

instance noZeroDivisors : NoZeroDivisors Ordinal :=
  ⟨fun {_ _} => mul_eq_zero'.1⟩

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

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

Разделы

Аффилиация

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