English
The representation of exponentiation in ONote corresponds to exponentiation of representations: repr(o1^o2) = repr(o1)^{repr(o2)} provided NF conditions on o1 and o2.
Русский
Представление операции возведения в степень в ONote соответствует возведению в степень по представлениям: repr(o1^o2) = repr(o1)^{repr(o2)} при NF-условиях на o1 и o2.
LaTeX
$$$\\forall o_1\\,o_2\\,[NF\\ o_1]\\,[NF\\ o_2]\\; \\operatorname{repr}(o_1^{o_2}) = \\operatorname{repr}(o_1)^{\\operatorname{repr}(o_2)}$$$
Lean4
theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o₁ ^ repr o₂ :=
by
rcases e₁ : split o₁ with ⟨a, m⟩
obtain ⟨N₁, r₁⟩ := nf_repr_split e₁
obtain - | ⟨a0, n, a'⟩ := a
· rcases m with - | m
· by_cases h : o₂ = 0 <;> simp [opow_def, opowAux2, e₁, h, r₁]
have := mt repr_inj.1 h
rw [zero_opow this]
· rcases e₂ : split' o₂ with ⟨b', k⟩
obtain ⟨_, r₂⟩ := nf_repr_split' e₂
by_cases h : m = 0
· simp [opowAux2, opow_def, e₁, h, r₁, r₂]
simp only [opow_def, opowAux2, e₁, r₁, e₂, r₂, repr, Nat.cast_succ, _root_.zero_add, add_zero]
rw [opow_add, opow_mul, opow_omega0, add_one_eq_succ]
· simp
· simpa [Nat.one_le_iff_ne_zero]
· rw [← Nat.cast_succ, lt_omega0]
exact ⟨_, rfl⟩
· haveI := N₁.fst
haveI := N₁.snd
obtain ⟨a00, ad⟩ := N₁.of_dvd_omega0 (split_dvd e₁)
have al := split_add_lt e₁
have aa : repr (a' + ofNat m) = repr a' + m := by simp only [ONote.repr_ofNat, ONote.repr_add]
rcases e₂ : split' o₂ with ⟨b', k⟩
obtain ⟨_, r₂⟩ := nf_repr_split' e₂
simp only [opow_def, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr]
rcases k with - | k
· simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]
· simp [r₂, opow_add, opow_mul, mul_assoc, add_assoc]
rw [repr_opow_aux₁ a00 al aa, scale_opowAux]
simp only [repr_mul, repr_scale, repr, opow_zero, PNat.val_ofNat, Nat.cast_one, mul_one, add_zero, opow_one,
opow_mul]
rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))]
congr 1
rw [← pow_succ, ← opow_natCast, ← opow_natCast]
exact (repr_opow_aux₂ _ ad a00 al _ _).2
