div_self

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For any ordinal a ≠ 0, a / a = 1.

Русский

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

LaTeX

$$$a \\\\neq 0 \\\\Rightarrow a / a = 1$$$

Lean4

@[simp]
theorem div_self {a : Ordinal} (h : a ≠ 0) : a / a = 1 := by simpa only [mul_one] using mul_div_cancel 1 h

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

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

Разделы

Аффилиация

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