zero_mod

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For any ordinal b, 0 % b = 0.

Русский

Для любого ординала b, 0 % b = 0.

LaTeX

$$∀ b ∈ \\operatorname{Ord}, 0 % b = 0$$

Lean4

@[simp]
theorem zero_mod (b : Ordinal) : 0 % b = 0 := by simp only [mod_def, zero_div, mul_zero, sub_self]

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

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

Разделы

Аффилиация

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