no goals
S : Type ?u.864368
T : Type ?u.864371
R : Type u_1
inst✝ : CommRing R
r✝ x y z : R
a b c : ℍ[R]
r : R
q : ℍ[R]
⊢ ↑normSq (r • q) = r ^ 2 * ↑normSq q
simp only [normSq_def', smul_re, smul_imI, smul_imJ, smul_imK, mul_pow, mul_add, smul_eq_mul]