feat(data/matrix/notation): relax typeclass assumptions (#11429)

src/data/matrix/notation.lean

@@ -249,16 +249,16 @@ lemma vec3_add [has_add α] (a₀ a₁ a₂ b₀ b₁ b₂ : α) :
   ![a₀, a₁, a₂] + ![b₀, b₁, b₂] = ![a₀ + b₀, a₁ + b₁, a₂ + b₂] :=
 by rw [cons_add_cons, cons_add_cons, cons_add_cons, empty_add_empty]
 
-variable [semiring α]
-
-lemma smul_vec2 (x : α) (a₀ a₁ : α) :
+lemma smul_vec2 {R : Type*} [has_scalar R α] (x : R) (a₀ a₁ : α) :
   x • ![a₀, a₁] = ![x • a₀, x • a₁] :=
 by rw [smul_cons, smul_cons, smul_empty]
 
-lemma smul_vec3 (x : α) (a₀ a₁ a₂ : α) :
+lemma smul_vec3 {R : Type*} [has_scalar R α] (x : R) (a₀ a₁ a₂ : α) :
   x • ![a₀, a₁, a₂] = ![x • a₀, x • a₁, x • a₂] :=
 by rw [smul_cons, smul_cons, smul_cons, smul_empty]
 
+variables [add_comm_monoid α] [has_mul α]
+
 lemma vec2_dot_product' {a₀ a₁ b₀ b₁ : α} :
   ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁ :=
 by rw [cons_dot_product_cons, cons_dot_product_cons, dot_product_empty, add_zero]

src/linear_algebra/cross_product.lean

@@ -49,13 +49,13 @@ begin
       a 2 * b 0 - a 0 * b 2,
       a 0 * b 1 - a 1 * b 0]),
   { intros,
-    simp [@vec3_add R _ _ _ _ _ _ _, add_comm, add_assoc, add_left_comm, add_mul, sub_eq_add_neg] },
+    simp [vec3_add (_ : R), add_comm, add_assoc, add_left_comm, add_mul, sub_eq_add_neg] },
   { intros,
-    simp [smul_vec3, mul_comm, mul_assoc, mul_left_comm, mul_add, sub_eq_add_neg] },
+    simp [smul_vec3 (_ : R) (_ : R), mul_comm, mul_assoc, mul_left_comm, mul_add, sub_eq_add_neg] },
   { intros,
-    simp [@vec3_add R _ _ _ _ _ _ _, add_comm, add_assoc, add_left_comm, mul_add, sub_eq_add_neg] },
+    simp [vec3_add (_ : R), add_comm, add_assoc, add_left_comm, mul_add, sub_eq_add_neg] },
   { intros,
-    simp [smul_vec3, mul_comm, mul_assoc, mul_left_comm, mul_add, sub_eq_add_neg] },
+    simp [smul_vec3 (_ : R) (_ : R), mul_comm, mul_assoc, mul_left_comm, mul_add, sub_eq_add_neg] },
 end
 
 localized "infixl ` ×₃ `: 74 := cross_product" in matrix