opow_mul — Mathlib

English

For ordinals a,b,c, a^{b·c} = (a^b)^c.

Русский

Для ординалов a,b,c выполняется a^{b·c} = (a^b)^c.

LaTeX

$$$a^{(b \cdot c)} = (a^{b})^{c}$$$

Lean4

theorem opow_mul (a b c : Ordinal) : a ^ (b * c) = (a ^ b) ^ c :=
  by
  by_cases b0 : b = 0; · simp only [b0, zero_mul, opow_zero, one_opow]
  by_cases a0 : a = 0
  · subst a
    by_cases c0 : c = 0
    · simp only [c0, mul_zero, opow_zero]
    simp only [zero_opow b0, zero_opow c0, zero_opow (mul_ne_zero b0 c0)]
  rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with a1 | a1
  · subst a1
    simp only [one_opow]
  induction c using limitRecOn with
  | zero => simp only [mul_zero, opow_zero]
  | succ c IH => rw [mul_succ, opow_add, IH, opow_succ]
  | limit c l
    IH =>
    refine
      eq_of_forall_ge_iff fun d =>
        (((isNormal_opow a1).trans (isNormal_mul_right (Ordinal.pos_iff_ne_zero.2 b0))).limit_le l).trans ?_
    dsimp only [Function.comp_def]
    simp +contextual only [IH]
    exact (opow_le_of_isSuccLimit (opow_ne_zero _ a0) l).symm

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