one_opow — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by
  induction a using limitRecOn with
  | zero => simp only [opow_zero]
  | succ _ ih => simp only [opow_succ, ih, mul_one]
  | limit b l IH =>
    refine eq_of_forall_ge_iff fun c => ?_
    rw [opow_le_of_isSuccLimit Ordinal.one_ne_zero l]
    exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩

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