1.4. Scalar multiplication🔗

namespace SMul

-- extend scalar multiplication on ℚ to
-- scalar multiplication on ℚ[i]
scoped instance instSMulRationalComplex {R : Type*}
  [SMul R ℚ] : SMul R ℚ[i] where
  smul r x := ⟨r • x.re - 0 * x.im, r • x.im + 0 * x.re⟩

end SMul

open scoped SMul

section SMul

variable {R : Type*} [SMul R ℚ]

theorem smul_re (r : R) (z : ℚ[i])
  : (r • z).re = r • z.re := byR:Type u_1inst✝:SMul R ℚr:Rz:ℚ[i]⊢ (r • z).re = r • z.re simp [(· • ·), SMul.smul]All goals completed! 🐙

theorem smul_im (r : R) (z : ℚ[i])
  : (r • z).im = r • z.im := byR:Type u_1inst✝:SMul R ℚr:Rz:ℚ[i]⊢ (r • z).im = r • z.im simp [(· • ·), SMul.smul]All goals completed! 🐙

@[simp]
theorem rational_smul {x : ℚ} {z : ℚ[i]} : x • z = x * z :=
  rfl

end SMul