chore(data/fin/vec_notation): generalize smul_cons (#11285)

Author: eric-wieser

src/data/complex/module.lean

@@ -125,7 +125,8 @@ basis.of_equiv_fun
   left_inv := λ z, by simp,
   right_inv := λ c, by { ext i, fin_cases i; simp },
   map_add' := λ z z', by simp,
-  map_smul' := λ c z, by simp }
+  -- why does `simp` not know how to apply `smul_cons`, which is a `@[simp]` lemma, here?
+  map_smul' := λ c z, by simp [matrix.smul_cons c z.re, matrix.smul_cons c z.im] }
 
 @[simp] lemma coe_basis_one_I_repr (z : ℂ) : ⇑(basis_one_I.repr z) = ![z.re, z.im] := rfl
 

src/data/fin/vec_notation.lean

@@ -274,14 +274,12 @@ end val
 
 section smul
 
-variables [semiring α]
--- TODO: if I generalize these lemmas to `[has_scalar M α]`, then Lean fails to apply them
--- in `data.complex.module`
+variables {M : Type*} [has_scalar M α]
 
-@[simp] lemma smul_empty (x : α) (v : fin 0 → α) : x • v = ![] := empty_eq _
+@[simp] lemma smul_empty (x : M) (v : fin 0 → α) : x • v = ![] := empty_eq _
 
-@[simp] lemma smul_cons (x y : α) (v : fin n → α) :
-  x • vec_cons y v = vec_cons (x * y) (x • v) :=
+@[simp] lemma smul_cons (x : M) (y : α) (v : fin n → α) :
+  x • vec_cons y v = vec_cons (x • y) (x • v) :=
 by { ext i, refine fin.cases _ _ i; simp }
 
 end smul