English
For ordinals a,b,c, the exponential distributes over addition: a^{b+c} = a^b · a^c.
Русский
Пусть a,b,c — ординалы. Тогда a^{b+c} = a^b · a^c.
LaTeX
$$$a^{(b+c)} = a^{b} \cdot a^{c}$$$
Lean4
theorem opow_add (a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c :=
by
rcases eq_or_ne a 0 with (rfl | a0)
· rcases eq_or_ne c 0 with (rfl | c0)
· simp
have : b + c ≠ 0 := ((Ordinal.pos_iff_ne_zero.2 c0).trans_le (le_add_left _ _)).ne'
simp only [zero_opow c0, zero_opow this, mul_zero]
rcases eq_or_lt_of_le (one_le_iff_ne_zero.2 a0) with (rfl | a1)
· simp only [one_opow, mul_one]
induction c using limitRecOn with
| zero => simp
| succ c IH => rw [add_succ, opow_succ, IH, opow_succ, mul_assoc]
| limit c l
IH =>
refine eq_of_forall_ge_iff fun d => (((isNormal_opow a1).trans (isNormal_add_right b)).limit_le l).trans ?_
dsimp only [Function.comp_def]
simp +contextual only [IH]
exact (((isNormal_mul_right <| opow_pos b (Ordinal.pos_iff_ne_zero.2 a0)).trans (isNormal_opow a1)).limit_le l).symm
