English
Scaling a quaternion scales its norm quadratically: normSq(r • q) = r^2 · normSq(q).
Русский
Умножение квартониона на скаляр масштабирует норму квадратично: normSq(r • q) = r^2 · normSq(q).
LaTeX
$$$\operatorname{normSq}(r \cdot q) = r^2 \cdot \operatorname{normSq}(q)$$$
Lean4
theorem normSq_smul (r : R) (q : ℍ[R]) : normSq (r • q) = r ^ 2 * normSq q := by
simp only [normSq_def', re_smul, imI_smul, imJ_smul, imK_smul, mul_pow, mul_add, smul_eq_mul]