opow_one

Mathlib.SetTheory.Ordinal.Exponential

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

English

For any ordinal a, a raised to the power 1 equals a.

Русский

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

LaTeX

$$$\forall a : \mathrm{Ordinal},\ a^{(1)} = a$$$

Lean4

@[simp]
theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a :=
  by
  rw [← succ_zero, opow_succ]
  simp only [opow_zero, one_mul]

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

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

Разделы

Аффилиация

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