English
For ONote e, a0, a, and natural k,m with NF assumptions, the representation scales multiplicatively: repr(opowAux(e,a0,a,k,m)) = ω^{repr e} · repr(opowAux(0,a0,a,k,m)).
Русский
Для ONote e, a0, a и натуральных k,m при условии NF, представление масштабируется умножением: repr(opowAux(e,a0,a,k,m)) = ω^{repr e} · repr(opowAux(0,a0,a,k,m)).
LaTeX
$$$\\forall e\\,a_0\\,a\\,[NF\\ e][NF\\ a_0][NF\\ a]\\;\\forall k,m:\\; \\operatorname{repr}(\\operatorname{opowAux}(e,a_0,a,k,m)) = \\omega^{\\operatorname{repr} e} \\cdot \\operatorname{repr}(\\operatorname{opowAux}(0,a_0,a,k,m))$$$
Lean4
theorem scale_opowAux (e a0 a : ONote) [NF e] [NF a0] [NF a] :
∀ k m, repr (opowAux e a0 a k m) = ω ^ repr e * repr (opowAux 0 a0 a k m)
| 0, m => by cases m <;> simp [opowAux]
| k + 1, m => by
by_cases h : m = 0 <;>
simp only [h, opowAux, mulNat_eq_mul, repr_add, repr_scale, repr_mul, repr_ofNat, zero_add, mul_add, repr_zero,
mul_zero, scale_opowAux e, opow_add, mul_assoc]
