mod_self

Mathlib.SetTheory.Ordinal.Arithmetic

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

← MathLib Explorer

English

For any ordinal a, a % a = 0.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem mod_self (a : Ordinal) : a % a = 0 :=
  if a0 : a = 0 then by simp only [a0, zero_mod] else by simp only [mod_def, div_self a0, mul_one, sub_self]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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