normSq_smul — Mathlib

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]

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