diff --git a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
index d3c8426182c8b..c5f18e52474a1 100644
--- a/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
+++ b/Archive/Wiedijk100Theorems/FriendshipGraphs.lean
@@ -178,7 +178,7 @@ theorem isRegularOf_not_existsPolitician (hG' : ¬ExistsPolitician G) :
   This essentially means that the graph has `d ^ 2 - d + 1` vertices. -/
 theorem card_of_regular (hd : G.IsRegularOfDegree d) : d + (Fintype.card V - 1) = d * d := by
   have v := Classical.arbitrary V
-  trans (G.adjMatrix ℕ ^ 2).mulVec (fun _ => 1) v
+  trans ((G.adjMatrix ℕ ^ 2) *ᵥ (fun _ => 1)) v
   · rw [adjMatrix_sq_of_regular hG hd, mulVec, dotProduct, ← insert_erase (mem_univ v)]
     simp only [sum_insert, mul_one, if_true, Nat.cast_id, eq_self_iff_true, mem_erase, not_true,
       Ne.def, not_false_iff, add_right_inj, false_and_iff, of_apply]
diff --git a/Mathlib/Analysis/Matrix.lean b/Mathlib/Analysis/Matrix.lean
index 6e10f9b8c44d1..7db0428d46eb2 100644
--- a/Mathlib/Analysis/Matrix.lean
+++ b/Mathlib/Analysis/Matrix.lean
@@ -380,8 +380,8 @@ theorem linfty_opNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖
 alias linfty_op_norm_mul :=
   linfty_opNorm_mul -- deprecated on 2024-02-02
 
-theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A.mulVec v‖₊ ≤ ‖A‖₊ * ‖v‖₊ := by
-  rw [← linfty_opNNNorm_col (A.mulVec v), ← linfty_opNNNorm_col v]
+theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖₊ ≤ ‖A‖₊ * ‖v‖₊ := by
+  rw [← linfty_opNNNorm_col (A *ᵥ v), ← linfty_opNNNorm_col v]
   exact linfty_opNNNorm_mul A (col v)
 #align matrix.linfty_op_nnnorm_mul_vec Matrix.linfty_opNNNorm_mulVec
 
@@ -389,7 +389,7 @@ theorem linfty_opNNNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A.mulVec
 alias linfty_op_nnnorm_mulVec :=
   linfty_opNNNorm_mulVec -- deprecated on 2024-02-02
 
-theorem linfty_opNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖Matrix.mulVec A v‖ ≤ ‖A‖ * ‖v‖ :=
+theorem linfty_opNorm_mulVec (A : Matrix l m α) (v : m → α) : ‖A *ᵥ v‖ ≤ ‖A‖ * ‖v‖ :=
   linfty_opNNNorm_mulVec _ _
 #align matrix.linfty_op_norm_mul_vec Matrix.linfty_opNorm_mulVec
 
diff --git a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean
index 4cb65d92e0dfe..9edc99cf95ebd 100644
--- a/Mathlib/Analysis/NormedSpace/Star/Matrix.lean
+++ b/Mathlib/Analysis/NormedSpace/Star/Matrix.lean
@@ -220,7 +220,7 @@ alias l2_op_nnnorm_conjTranspose_mul_self :=
 
 -- note: with only a type ascription in the left-hand side, Lean picks the wrong norm.
 lemma l2_opNorm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
-    ‖(EuclideanSpace.equiv m 𝕜).symm <| A.mulVec x‖ ≤ ‖A‖ * ‖x‖ :=
+    ‖(EuclideanSpace.equiv m 𝕜).symm <| A *ᵥ x‖ ≤ ‖A‖ * ‖x‖ :=
   toEuclideanLin (n := n) (m := m) (𝕜 := 𝕜) |>.trans toContinuousLinearMap A |>.le_opNorm x
 
 @[deprecated l2_opNorm_mulVec]
@@ -228,7 +228,7 @@ alias l2_op_norm_mulVec :=
   l2_opNorm_mulVec -- deprecated on 2024-02-02
 
 lemma l2_opNNNorm_mulVec (A : Matrix m n 𝕜) (x : EuclideanSpace 𝕜 n) :
-    ‖(EuclideanSpace.equiv m 𝕜).symm <| A.mulVec x‖₊ ≤ ‖A‖₊ * ‖x‖₊ :=
+    ‖(EuclideanSpace.equiv m 𝕜).symm <| A *ᵥ x‖₊ ≤ ‖A‖₊ * ‖x‖₊ :=
   A.l2_opNorm_mulVec x
 
 @[deprecated l2_opNNNorm_mulVec]
diff --git a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
index e280ac8f92672..6e40507658026 100644
--- a/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
@@ -209,13 +209,13 @@ theorem dotProduct_adjMatrix [NonAssocSemiring α] (v : V) (vec : V → α) :
 
 @[simp]
 theorem adjMatrix_mulVec_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
-    ((G.adjMatrix α).mulVec vec) v = ∑ u in G.neighborFinset v, vec u := by
+    (G.adjMatrix α *ᵥ vec) v = ∑ u in G.neighborFinset v, vec u := by
   rw [mulVec, adjMatrix_dotProduct]
 #align simple_graph.adj_matrix_mul_vec_apply SimpleGraph.adjMatrix_mulVec_apply
 
 @[simp]
 theorem adjMatrix_vecMul_apply [NonAssocSemiring α] (v : V) (vec : V → α) :
-    ((G.adjMatrix α).vecMul vec) v = ∑ u in G.neighborFinset v, vec u := by
+    (vec ᵥ* G.adjMatrix α) v = ∑ u in G.neighborFinset v, vec u := by
   simp only [← dotProduct_adjMatrix, vecMul]
   refine' congr rfl _; ext x
   rw [← transpose_apply (adjMatrix α G) x v, transpose_adjMatrix]
@@ -250,11 +250,11 @@ variable {G}
 
 -- @[simp] -- Porting note: simp can prove this
 theorem adjMatrix_mulVec_const_apply [Semiring α] {a : α} {v : V} :
-    (G.adjMatrix α).mulVec (Function.const _ a) v = G.degree v * a := by simp
+    (G.adjMatrix α *ᵥ Function.const _ a) v = G.degree v * a := by simp
 #align simple_graph.adj_matrix_mul_vec_const_apply SimpleGraph.adjMatrix_mulVec_const_apply
 
 theorem adjMatrix_mulVec_const_apply_of_regular [Semiring α] {d : ℕ} {a : α}
-    (hd : G.IsRegularOfDegree d) {v : V} : (G.adjMatrix α).mulVec (Function.const _ a) v = d * a :=
+    (hd : G.IsRegularOfDegree d) {v : V} : (G.adjMatrix α *ᵥ Function.const _ a) v = d * a :=
   by simp [hd v]
 #align simple_graph.adj_matrix_mul_vec_const_apply_of_regular SimpleGraph.adjMatrix_mulVec_const_apply_of_regular
 
diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
index 4951176df2d6a..fce24a84d230e 100644
--- a/Mathlib/Data/Matrix/Basic.lean
+++ b/Mathlib/Data/Matrix/Basic.lean
@@ -32,6 +32,8 @@ with `Matrix m n α`. For the typical approach of counting rows and columns,
 The locale `Matrix` gives the following notation:
 
 * `⬝ᵥ` for `Matrix.dotProduct`
+* `*ᵥ` for `Matrix.mulVec`
+* `ᵥ*` for `Matrix.vecMul`
 * `ᵀ` for `Matrix.transpose`
 * `ᴴ` for `Matrix.conjTranspose`
 
@@ -1677,24 +1679,40 @@ section NonUnitalNonAssocSemiring
 
 variable [NonUnitalNonAssocSemiring α]
 
-/-- `mulVec M v` is the matrix-vector product of `M` and `v`, where `v` is seen as a column matrix.
-    Put another way, `mulVec M v` is the vector whose entries
-    are those of `M * col v` (see `col_mulVec`). -/
+/--
+`M *ᵥ v` (notation for `mulVec M v`) is the matrix-vector product of matrix `M` and vector `v`,
+where `v` is seen as a column vector.
+Put another way, `M *ᵥ v` is the vector whose entries are those of `M * col v` (see `col_mulVec`).
+
+The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `Matrix.dotProduct`,
+so that `A *ᵥ v ⬝ᵥ B *ᵥ w` is parsed as `(A *ᵥ v) ⬝ᵥ (B *ᵥ w)`.
+-/
 def mulVec [Fintype n] (M : Matrix m n α) (v : n → α) : m → α
   | i => (fun j => M i j) ⬝ᵥ v
 #align matrix.mul_vec Matrix.mulVec
 
-/-- `vecMul v M` is the vector-matrix product of `v` and `M`, where `v` is seen as a row matrix.
-    Put another way, `vecMul v M` is the vector whose entries
-    are those of `row v * M` (see `row_vecMul`). -/
+@[inherit_doc]
+scoped infixr:73 " *ᵥ " => Matrix.mulVec
+
+/--
+`v ᵥ* M` (notation for `vecMul v M`) is the vector-matrix product of vector `v` and matrix `M`,
+where `v` is seen as a row vector.
+Put another way, `v ᵥ* M` is the vector whose entries are those of `row v * M` (see `row_vecMul`).
+
+The notation has precedence 73, which comes immediately before ` ⬝ᵥ ` for `Matrix.dotProduct`,
+so that `v ᵥ* A ⬝ᵥ w ᵥ* B` is parsed as `(v ᵥ* A) ⬝ᵥ (w ᵥ* B)`.
+-/
 def vecMul [Fintype m] (v : m → α) (M : Matrix m n α) : n → α
   | j => v ⬝ᵥ fun i => M i j
 #align matrix.vec_mul Matrix.vecMul
 
+@[inherit_doc]
+scoped infixl:73 " ᵥ* " => Matrix.vecMul
+
 /-- Left multiplication by a matrix, as an `AddMonoidHom` from vectors to vectors. -/
 @[simps]
 def mulVec.addMonoidHomLeft [Fintype n] (v : n → α) : Matrix m n α →+ m → α where
-  toFun M := mulVec M v
+  toFun M := M *ᵥ v
   map_zero' := by
     ext
     simp [mulVec]
@@ -1705,109 +1723,109 @@ def mulVec.addMonoidHomLeft [Fintype n] (v : n → α) : Matrix m n α →+ m 
 
 /-- The `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`. -/
 theorem mul_apply_eq_vecMul [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) :
-    (A * B) i = vecMul (A i) B :=
+    (A * B) i = A i ᵥ* B :=
   rfl
 
 theorem mulVec_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
-    mulVec (diagonal v) w x = v x * w x :=
+    (diagonal v *ᵥ w) x = v x * w x :=
   diagonal_dotProduct v w x
 #align matrix.mul_vec_diagonal Matrix.mulVec_diagonal
 
 theorem vecMul_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
-    vecMul v (diagonal w) x = v x * w x :=
+    (v ᵥ* diagonal w) x = v x * w x :=
   dotProduct_diagonal' v w x
 #align matrix.vec_mul_diagonal Matrix.vecMul_diagonal
 
 /-- Associate the dot product of `mulVec` to the left. -/
 theorem dotProduct_mulVec [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R)
-    (A : Matrix m n R) (w : n → R) : v ⬝ᵥ mulVec A w = vecMul v A ⬝ᵥ w := by
+    (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w := by
   simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]
   exact Finset.sum_comm
 #align matrix.dot_product_mul_vec Matrix.dotProduct_mulVec
 
 @[simp]
-theorem mulVec_zero [Fintype n] (A : Matrix m n α) : mulVec A 0 = 0 := by
+theorem mulVec_zero [Fintype n] (A : Matrix m n α) : A *ᵥ 0 = 0 := by
   ext
   simp [mulVec]
 #align matrix.mul_vec_zero Matrix.mulVec_zero
 
 @[simp]
-theorem zero_vecMul [Fintype m] (A : Matrix m n α) : vecMul 0 A = 0 := by
+theorem zero_vecMul [Fintype m] (A : Matrix m n α) : 0 ᵥ* A = 0 := by
   ext
   simp [vecMul]
 #align matrix.zero_vec_mul Matrix.zero_vecMul
 
 @[simp]
-theorem zero_mulVec [Fintype n] (v : n → α) : mulVec (0 : Matrix m n α) v = 0 := by
+theorem zero_mulVec [Fintype n] (v : n → α) : (0 : Matrix m n α) *ᵥ v = 0 := by
   ext
   simp [mulVec]
 #align matrix.zero_mul_vec Matrix.zero_mulVec
 
 @[simp]
-theorem vecMul_zero [Fintype m] (v : m → α) : vecMul v (0 : Matrix m n α) = 0 := by
+theorem vecMul_zero [Fintype m] (v : m → α) : v ᵥ* (0 : Matrix m n α) = 0 := by
   ext
   simp [vecMul]
 #align matrix.vec_mul_zero Matrix.vecMul_zero
 
 theorem smul_mulVec_assoc [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α]
-    (a : R) (A : Matrix m n α) (b : n → α) : (a • A).mulVec b = a • A.mulVec b := by
+    (a : R) (A : Matrix m n α) (b : n → α) : (a • A) *ᵥ b = a • A *ᵥ b := by
   ext
   apply smul_dotProduct
 #align matrix.smul_mul_vec_assoc Matrix.smul_mulVec_assoc
 
 theorem mulVec_add [Fintype n] (A : Matrix m n α) (x y : n → α) :
-    A.mulVec (x + y) = A.mulVec x + A.mulVec y := by
+    A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y := by
   ext
   apply dotProduct_add
 #align matrix.mul_vec_add Matrix.mulVec_add
 
 theorem add_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
-    (A + B).mulVec x = A.mulVec x + B.mulVec x := by
+    (A + B) *ᵥ x = A *ᵥ x + B *ᵥ x := by
   ext
   apply add_dotProduct
 #align matrix.add_mul_vec Matrix.add_mulVec
 
 theorem vecMul_add [Fintype m] (A B : Matrix m n α) (x : m → α) :
-    vecMul x (A + B) = vecMul x A + vecMul x B := by
+    x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B := by
   ext
   apply dotProduct_add
 #align matrix.vec_mul_add Matrix.vecMul_add
 
 theorem add_vecMul [Fintype m] (A : Matrix m n α) (x y : m → α) :
-    vecMul (x + y) A = vecMul x A + vecMul y A := by
+    (x + y) ᵥ* A = x ᵥ* A + y ᵥ* A := by
   ext
   apply add_dotProduct
 #align matrix.add_vec_mul Matrix.add_vecMul
 
 theorem vecMul_smul [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S]
     [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : n → S) :
-    M.vecMul (b • v) = b • M.vecMul v := by
+    (b • v) ᵥ* M = b • v ᵥ* M := by
   ext i
   simp only [vecMul, dotProduct, Finset.smul_sum, Pi.smul_apply, smul_mul_assoc]
 #align matrix.vec_mul_smul Matrix.vecMul_smul
 
 theorem mulVec_smul [Fintype n] [Monoid R] [NonUnitalNonAssocSemiring S] [DistribMulAction R S]
     [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : n → S) :
-    M.mulVec (b • v) = b • M.mulVec v := by
+    M *ᵥ (b • v) = b • M *ᵥ v := by
   ext i
   simp only [mulVec, dotProduct, Finset.smul_sum, Pi.smul_apply, mul_smul_comm]
 #align matrix.mul_vec_smul Matrix.mulVec_smul
 
 @[simp]
 theorem mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R)
-    (j : n) (x : R) : M.mulVec (Pi.single j x) = fun i => M i j * x :=
+    (j : n) (x : R) : M *ᵥ Pi.single j x = fun i => M i j * x :=
   funext fun _ => dotProduct_single _ _ _
 #align matrix.mul_vec_single Matrix.mulVec_single
 
 @[simp]
 theorem single_vecMul [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R)
-    (i : m) (x : R) : vecMul (Pi.single i x) M = fun j => x * M i j :=
+    (i : m) (x : R) : Pi.single i x ᵥ* M = fun j => x * M i j :=
   funext fun _ => single_dotProduct _ _ _
 #align matrix.single_vec_mul Matrix.single_vecMul
 
 -- @[simp] -- Porting note: not in simpNF
 theorem diagonal_mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
-    (j : n) (x : R) : (diagonal v).mulVec (Pi.single j x) = Pi.single j (v j * x) := by
+    (j : n) (x : R) : diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x) := by
   ext i
   rw [mulVec_diagonal]
   exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i
@@ -1815,7 +1833,7 @@ theorem diagonal_mulVec_single [Fintype n] [DecidableEq n] [NonUnitalNonAssocSem
 
 -- @[simp] -- Porting note: not in simpNF
 theorem single_vecMul_diagonal [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : n → R)
-    (j : n) (x : R) : vecMul (Pi.single j x) (diagonal v) = Pi.single j (x * v j) := by
+    (j : n) (x : R) : (Pi.single j x) ᵥ* (diagonal v) = Pi.single j (x * v j) := by
   ext i
   rw [vecMul_diagonal]
   exact Pi.apply_single (fun i x => x * v i) (fun i => zero_mul _) j x i
@@ -1829,41 +1847,41 @@ variable [NonUnitalSemiring α]
 
 @[simp]
 theorem vecMul_vecMul [Fintype n] [Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α) :
-    vecMul (vecMul v M) N = vecMul v (M * N) := by
+    v ᵥ* M ᵥ* N = v ᵥ* (M * N) := by
   ext
   apply dotProduct_assoc
 #align matrix.vec_mul_vec_mul Matrix.vecMul_vecMul
 
 @[simp]
 theorem mulVec_mulVec [Fintype n] [Fintype o] (v : o → α) (M : Matrix m n α) (N : Matrix n o α) :
-    mulVec M (mulVec N v) = mulVec (M * N) v := by
+    M *ᵥ N *ᵥ v = (M * N) *ᵥ v := by
   ext
   symm
   apply dotProduct_assoc
 #align matrix.mul_vec_mul_vec Matrix.mulVec_mulVec
 
 theorem star_mulVec [Fintype n] [StarRing α] (M : Matrix m n α) (v : n → α) :
-    star (M.mulVec v) = vecMul (star v) Mᴴ :=
+    star (M *ᵥ v) = star v ᵥ* Mᴴ :=
   funext fun _ => (star_dotProduct_star _ _).symm
 #align matrix.star_mul_vec Matrix.star_mulVec
 
 theorem star_vecMul [Fintype m] [StarRing α] (M : Matrix m n α) (v : m → α) :
-    star (M.vecMul v) = Mᴴ.mulVec (star v) :=
+    star (v ᵥ* M) = Mᴴ *ᵥ star v :=
   funext fun _ => (star_dotProduct_star _ _).symm
 #align matrix.star_vec_mul Matrix.star_vecMul
 
 theorem mulVec_conjTranspose [Fintype m] [StarRing α] (A : Matrix m n α) (x : m → α) :
-    mulVec Aᴴ x = star (vecMul (star x) A) :=
+    Aᴴ *ᵥ x = star (star x ᵥ* A) :=
   funext fun _ => star_dotProduct _ _
 #align matrix.mul_vec_conj_transpose Matrix.mulVec_conjTranspose
 
 theorem vecMul_conjTranspose [Fintype n] [StarRing α] (A : Matrix m n α) (x : n → α) :
-    vecMul x Aᴴ = star (mulVec A (star x)) :=
+    x ᵥ* Aᴴ = star (A *ᵥ star x) :=
   funext fun _ => dotProduct_star _ _
 #align matrix.vec_mul_conj_transpose Matrix.vecMul_conjTranspose
 
 theorem mul_mul_apply [Fintype n] (A B C : Matrix n n α) (i j : n) :
-    (A * B * C) i j = A i ⬝ᵥ B.mulVec (Cᵀ j) := by
+    (A * B * C) i j = A i ⬝ᵥ B *ᵥ (Cᵀ j) := by
   rw [Matrix.mul_assoc]
   simp only [mul_apply, dotProduct, mulVec]
   rfl
@@ -1875,24 +1893,24 @@ section NonAssocSemiring
 
 variable [NonAssocSemiring α]
 
-theorem mulVec_one [Fintype n] (A : Matrix m n α) : mulVec A 1 = fun i => ∑ j, A i j := by
+theorem mulVec_one [Fintype n] (A : Matrix m n α) : A *ᵥ 1 = fun i => ∑ j, A i j := by
   ext; simp [mulVec, dotProduct]
 #align matrix.mul_vec_one Matrix.mulVec_one
 
-theorem vec_one_mul [Fintype m] (A : Matrix m n α) : vecMul 1 A = fun j => ∑ i, A i j := by
+theorem vec_one_mul [Fintype m] (A : Matrix m n α) : 1 ᵥ* A = fun j => ∑ i, A i j := by
   ext; simp [vecMul, dotProduct]
 #align matrix.vec_one_mul Matrix.vec_one_mul
 
 variable [Fintype m] [Fintype n] [DecidableEq m]
 
 @[simp]
-theorem one_mulVec (v : m → α) : mulVec 1 v = v := by
+theorem one_mulVec (v : m → α) : 1 *ᵥ v = v := by
   ext
   rw [← diagonal_one, mulVec_diagonal, one_mul]
 #align matrix.one_mul_vec Matrix.one_mulVec
 
 @[simp]
-theorem vecMul_one (v : m → α) : vecMul v 1 = v := by
+theorem vecMul_one (v : m → α) : v ᵥ* 1 = v := by
   ext
   rw [← diagonal_one, vecMul_diagonal, mul_one]
 #align matrix.vec_mul_one Matrix.vecMul_one
@@ -1903,32 +1921,32 @@ section NonUnitalNonAssocRing
 
 variable [NonUnitalNonAssocRing α]
 
-theorem neg_vecMul [Fintype m] (v : m → α) (A : Matrix m n α) : vecMul (-v) A = -vecMul v A := by
+theorem neg_vecMul [Fintype m] (v : m → α) (A : Matrix m n α) : (-v) ᵥ* A = - (v ᵥ* A) := by
   ext
   apply neg_dotProduct
 #align matrix.neg_vec_mul Matrix.neg_vecMul
 
-theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : vecMul v (-A) = -vecMul v A := by
+theorem vecMul_neg [Fintype m] (v : m → α) (A : Matrix m n α) : v ᵥ* (-A) = - (v ᵥ* A) := by
   ext
   apply dotProduct_neg
 #align matrix.vec_mul_neg Matrix.vecMul_neg
 
-theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : mulVec (-A) v = -mulVec A v := by
+theorem neg_mulVec [Fintype n] (v : n → α) (A : Matrix m n α) : (-A) *ᵥ v = - (A *ᵥ v) := by
   ext
   apply neg_dotProduct
 #align matrix.neg_mul_vec Matrix.neg_mulVec
 
-theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : mulVec A (-v) = -mulVec A v := by
+theorem mulVec_neg [Fintype n] (v : n → α) (A : Matrix m n α) : A *ᵥ (-v) = - (A *ᵥ v) := by
   ext
   apply dotProduct_neg
 #align matrix.mul_vec_neg Matrix.mulVec_neg
 
 theorem sub_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
-    mulVec (A - B) x = mulVec A x - mulVec B x := by simp [sub_eq_add_neg, add_mulVec, neg_mulVec]
+    (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x := by simp [sub_eq_add_neg, add_mulVec, neg_mulVec]
 #align matrix.sub_mul_vec Matrix.sub_mulVec
 
 theorem vecMul_sub [Fintype m] (A B : Matrix m n α) (x : m → α) :
-    vecMul x (A - B) = vecMul x A - vecMul x B := by simp [sub_eq_add_neg, vecMul_add, vecMul_neg]
+    x ᵥ* (A - B) = x ᵥ* A - x ᵥ* B := by simp [sub_eq_add_neg, vecMul_add, vecMul_neg]
 #align matrix.vec_mul_sub Matrix.vecMul_sub
 
 end NonUnitalNonAssocRing
@@ -1937,22 +1955,22 @@ section NonUnitalCommSemiring
 
 variable [NonUnitalCommSemiring α]
 
-theorem mulVec_transpose [Fintype m] (A : Matrix m n α) (x : m → α) : mulVec Aᵀ x = vecMul x A := by
+theorem mulVec_transpose [Fintype m] (A : Matrix m n α) (x : m → α) : Aᵀ *ᵥ x = x ᵥ* A := by
   ext
   apply dotProduct_comm
 #align matrix.mul_vec_transpose Matrix.mulVec_transpose
 
-theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : vecMul x Aᵀ = mulVec A x := by
+theorem vecMul_transpose [Fintype n] (A : Matrix m n α) (x : n → α) : x ᵥ* Aᵀ = A *ᵥ x := by
   ext
   apply dotProduct_comm
 #align matrix.vec_mul_transpose Matrix.vecMul_transpose
 
 theorem mulVec_vecMul [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : o → α) :
-    mulVec A (vecMul x B) = mulVec (A * Bᵀ) x := by rw [← mulVec_mulVec, mulVec_transpose]
+    A *ᵥ (x ᵥ* B) = (A * Bᵀ) *ᵥ x := by rw [← mulVec_mulVec, mulVec_transpose]
 #align matrix.mul_vec_vec_mul Matrix.mulVec_vecMul
 
 theorem vecMul_mulVec [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : n → α) :
-    vecMul (mulVec A x) B = vecMul x (Aᵀ * B) := by rw [← vecMul_vecMul, vecMul_transpose]
+    (A *ᵥ x) ᵥ* B = x ᵥ* (Aᵀ * B) := by rw [← vecMul_vecMul, vecMul_transpose]
 #align matrix.vec_mul_mul_vec Matrix.vecMul_mulVec
 
 end NonUnitalCommSemiring
@@ -1962,7 +1980,7 @@ section CommSemiring
 variable [CommSemiring α]
 
 theorem mulVec_smul_assoc [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) :
-    A.mulVec (a • b) = a • A.mulVec b := by
+    A *ᵥ (a • b) = a • A *ᵥ b := by
   ext
   apply dotProduct_smul
 #align matrix.mul_vec_smul_assoc Matrix.mulVec_smul_assoc
@@ -2551,13 +2569,13 @@ theorem submatrix_mul_equiv [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α]
 
 theorem submatrix_mulVec_equiv [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α]
     (M : Matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) :
-    (M.submatrix e₁ e₂).mulVec v = M.mulVec (v ∘ e₂.symm) ∘ e₁ :=
+    M.submatrix e₁ e₂ *ᵥ v = (M *ᵥ (v ∘ e₂.symm)) ∘ e₁ :=
   funext fun _ => Eq.symm (dotProduct_comp_equiv_symm _ _ _)
 #align matrix.submatrix_mul_vec_equiv Matrix.submatrix_mulVec_equiv
 
 theorem submatrix_vecMul_equiv [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α]
     (M : Matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) :
-    vecMul v (M.submatrix e₁ e₂) = vecMul (v ∘ e₁.symm) M ∘ e₂ :=
+    v ᵥ* M.submatrix e₁ e₂ = ((v ∘ e₁.symm) ᵥ* M) ∘ e₂ :=
   funext fun _ => Eq.symm (comp_equiv_symm_dotProduct _ _ _)
 #align matrix.submatrix_vec_mul_equiv Matrix.submatrix_vecMul_equiv
 
@@ -2703,12 +2721,12 @@ theorem map_dotProduct [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S)
 #align ring_hom.map_dot_product RingHom.map_dotProduct
 
 theorem map_vecMul [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R)
-    (v : n → R) (i : m) : f (M.vecMul v i) = (M.map f).vecMul (f ∘ v) i := by
+    (v : n → R) (i : m) : f ((v ᵥ* M) i) =  ((f ∘ v) ᵥ* M.map f) i := by
   simp only [Matrix.vecMul, Matrix.map_apply, RingHom.map_dotProduct, Function.comp]
 #align ring_hom.map_vec_mul RingHom.map_vecMul
 
 theorem map_mulVec [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R)
-    (v : n → R) (i : m) : f (M.mulVec v i) = (M.map f).mulVec (f ∘ v) i := by
+    (v : n → R) (i : m) : f ((M *ᵥ v) i) = (M.map f *ᵥ (f ∘ v)) i := by
   simp only [Matrix.mulVec, Matrix.map_apply, RingHom.map_dotProduct, Function.comp]
 #align ring_hom.map_mul_vec RingHom.map_mulVec
 
diff --git a/Mathlib/Data/Matrix/Block.lean b/Mathlib/Data/Matrix/Block.lean
index d38dff2f76b27..0f5d9d0633fe2 100644
--- a/Mathlib/Data/Matrix/Block.lean
+++ b/Mathlib/Data/Matrix/Block.lean
@@ -256,18 +256,18 @@ theorem fromBlocks_multiply [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring 
 
 theorem fromBlocks_mulVec [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α)
     (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : Sum l m → α) :
-    mulVec (fromBlocks A B C D) x =
-      Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr))
-        (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr)) := by
+    (fromBlocks A B C D) *ᵥ x =
+      Sum.elim (A *ᵥ (x ∘ Sum.inl) + B *ᵥ (x ∘ Sum.inr))
+        (C *ᵥ (x ∘ Sum.inl) + D *ᵥ (x ∘ Sum.inr)) := by
   ext i
   cases i <;> simp [mulVec, dotProduct]
 #align matrix.from_blocks_mul_vec Matrix.fromBlocks_mulVec
 
 theorem vecMul_fromBlocks [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (A : Matrix n l α)
     (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : Sum n o → α) :
-    vecMul x (fromBlocks A B C D) =
-      Sum.elim (vecMul (x ∘ Sum.inl) A + vecMul (x ∘ Sum.inr) C)
-        (vecMul (x ∘ Sum.inl) B + vecMul (x ∘ Sum.inr) D) := by
+    x ᵥ* fromBlocks A B C D =
+      Sum.elim ((x ∘ Sum.inl) ᵥ* A + (x ∘ Sum.inr) ᵥ* C)
+        ((x ∘ Sum.inl) ᵥ* B + (x ∘ Sum.inr) ᵥ* D) := by
   ext i
   cases i <;> simp [vecMul, dotProduct]
 #align matrix.vec_mul_from_blocks Matrix.vecMul_fromBlocks
diff --git a/Mathlib/Data/Matrix/Hadamard.lean b/Mathlib/Data/Matrix/Hadamard.lean
index d6534df9ee9d8..2f1c11492f3b4 100644
--- a/Mathlib/Data/Matrix/Hadamard.lean
+++ b/Mathlib/Data/Matrix/Hadamard.lean
@@ -150,7 +150,7 @@ theorem sum_hadamard_eq : (∑ i : m, ∑ j : n, (A ⊙ B) i j) = trace (A * B
 #align matrix.sum_hadamard_eq Matrix.sum_hadamard_eq
 
 theorem dotProduct_vecMul_hadamard [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
-    dotProduct (vecMul v (A ⊙ B)) w = trace (diagonal v * A * (B * diagonal w)ᵀ) := by
+    dotProduct (v ᵥ* (A ⊙ B)) w = trace (diagonal v * A * (B * diagonal w)ᵀ) := by
   rw [← sum_hadamard_eq, Finset.sum_comm]
   simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]
 #align matrix.dot_product_vec_mul_hadamard Matrix.dotProduct_vecMul_hadamard
diff --git a/Mathlib/Data/Matrix/Notation.lean b/Mathlib/Data/Matrix/Notation.lean
index 13f2a3527df5b..4a8cf972937c4 100644
--- a/Mathlib/Data/Matrix/Notation.lean
+++ b/Mathlib/Data/Matrix/Notation.lean
@@ -266,7 +266,7 @@ theorem mul_val_succ [Fintype n'] (A : Matrix (Fin m.succ) n' α) (B : Matrix n'
 
 @[simp]
 theorem cons_mul [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α) :
-    of (vecCons v A) * B = of (vecCons (vecMul v B) (of.symm (of A * B))) := by
+    of (vecCons v A) * B = of (vecCons (v ᵥ* B) (of.symm (of A * B))) := by
   ext i j
   refine' Fin.cases _ _ i
   · rfl
@@ -280,32 +280,32 @@ section VecMul
 variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
-theorem empty_vecMul (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : vecMul v B = 0 :=
+theorem empty_vecMul (v : Fin 0 → α) (B : Matrix (Fin 0) o' α) : v ᵥ* B = 0 :=
   rfl
 #align matrix.empty_vec_mul Matrix.empty_vecMul
 
 @[simp]
-theorem vecMul_empty [Fintype n'] (v : n' → α) (B : Matrix n' (Fin 0) α) : vecMul v B = ![] :=
+theorem vecMul_empty [Fintype n'] (v : n' → α) (B : Matrix n' (Fin 0) α) : v ᵥ* B = ![] :=
   empty_eq _
 #align matrix.vec_mul_empty Matrix.vecMul_empty
 
 @[simp]
 theorem cons_vecMul (x : α) (v : Fin n → α) (B : Fin n.succ → o' → α) :
-    vecMul (vecCons x v) (of B) = x • vecHead B + vecMul v (of <| vecTail B) := by
+    vecCons x v ᵥ* of B = x • vecHead B + v ᵥ* of vecTail B := by
   ext i
   simp [vecMul]
 #align matrix.cons_vec_mul Matrix.cons_vecMul
 
 @[simp]
 theorem vecMul_cons (v : Fin n.succ → α) (w : o' → α) (B : Fin n → o' → α) :
-    vecMul v (of <| vecCons w B) = vecHead v • w + vecMul (vecTail v) (of B) := by
+    v ᵥ* of (vecCons w B) = vecHead v • w + vecTail v ᵥ* of B := by
   ext i
   simp [vecMul]
 #align matrix.vec_mul_cons Matrix.vecMul_cons
 
 -- @[simp] -- Porting note: simp can prove this
 theorem cons_vecMul_cons (x : α) (v : Fin n → α) (w : o' → α) (B : Fin n → o' → α) :
-    vecMul (vecCons x v) (of <| vecCons w B) = x • w + vecMul v (of B) := by simp
+    vecCons x v ᵥ* of (vecCons w B) = x • w + v ᵥ* of B := by simp
 #align matrix.cons_vec_mul_cons Matrix.cons_vecMul_cons
 
 end VecMul
@@ -315,25 +315,25 @@ section MulVec
 variable [NonUnitalNonAssocSemiring α]
 
 @[simp]
-theorem empty_mulVec [Fintype n'] (A : Matrix (Fin 0) n' α) (v : n' → α) : mulVec A v = ![] :=
+theorem empty_mulVec [Fintype n'] (A : Matrix (Fin 0) n' α) (v : n' → α) : A *ᵥ v = ![] :=
   empty_eq _
 #align matrix.empty_mul_vec Matrix.empty_mulVec
 
 @[simp]
-theorem mulVec_empty (A : Matrix m' (Fin 0) α) (v : Fin 0 → α) : mulVec A v = 0 :=
+theorem mulVec_empty (A : Matrix m' (Fin 0) α) (v : Fin 0 → α) : A *ᵥ v = 0 :=
   rfl
 #align matrix.mul_vec_empty Matrix.mulVec_empty
 
 @[simp]
 theorem cons_mulVec [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (w : n' → α) :
-    mulVec (of <| vecCons v A) w = vecCons (dotProduct v w) (mulVec (of A) w) := by
+    (of <| vecCons v A) *ᵥ w = vecCons (dotProduct v w) (of A *ᵥ w) := by
   ext i
   refine' Fin.cases _ _ i <;> simp [mulVec]
 #align matrix.cons_mul_vec Matrix.cons_mulVec
 
 @[simp]
 theorem mulVec_cons {α} [CommSemiring α] (A : m' → Fin n.succ → α) (x : α) (v : Fin n → α) :
-    mulVec (of A) (vecCons x v) = x • vecHead ∘ A + mulVec (of (vecTail ∘ A)) v := by
+    (of A) *ᵥ (vecCons x v) = x • vecHead ∘ A + (of (vecTail ∘ A)) *ᵥ v := by
   ext i
   simp [mulVec, mul_comm]
 #align matrix.mul_vec_cons Matrix.mulVec_cons
diff --git a/Mathlib/Data/Matrix/Reflection.lean b/Mathlib/Data/Matrix/Reflection.lean
index 24e37c30ed5e0..133d45fab4592 100644
--- a/Mathlib/Data/Matrix/Reflection.lean
+++ b/Mathlib/Data/Matrix/Reflection.lean
@@ -177,19 +177,19 @@ def mulVecᵣ [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (v : F
 ```lean
 example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
   !![a₁₁, a₁₂;
-     a₂₁, a₂₂].mulVec ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
+     a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
 (mulVecᵣ_eq _ _).symm
 ```
 -/
 @[simp]
 theorem mulVecᵣ_eq [NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) :
-    mulVecᵣ A v = A.mulVec v := by
+    mulVecᵣ A v = A *ᵥ v := by
   simp [mulVecᵣ, Function.comp]
   rfl
 #align matrix.mul_vecᵣ_eq Matrix.mulVecᵣ_eq
 
 example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
-    !![a₁₁, a₁₂; a₂₁, a₂₂].mulVec ![b₁, b₂] = ![a₁₁ * b₁ + a₁₂ * b₂, a₂₁ * b₁ + a₂₂ * b₂] :=
+    !![a₁₁, a₁₂; a₂₁, a₂₂] *ᵥ ![b₁, b₂] = ![a₁₁ * b₁ + a₁₂ * b₂, a₂₁ * b₁ + a₂₂ * b₂] :=
   (mulVecᵣ_eq _ _).symm
 
 /-- `Matrix.vecMul` with better defeq for `Fin` -/
@@ -200,20 +200,20 @@ def vecMulᵣ [Mul α] [Add α] [Zero α] (v : Fin l → α) (A : Matrix (Fin l)
 /-- This can be used to prove
 ```lean
 example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
-  vecMul ![b₁, b₂] !![a₁₁, a₁₂;
+  ![b₁, b₂] ᵥ* !![a₁₁, a₁₂;
                        a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
 (vecMulᵣ_eq _ _).symm
 ```
 -/
 @[simp]
 theorem vecMulᵣ_eq [NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α) :
-    vecMulᵣ v A = vecMul v A := by
+    vecMulᵣ v A = v ᵥ* A := by
   simp [vecMulᵣ, Function.comp]
   rfl
 #align matrix.vec_mulᵣ_eq Matrix.vecMulᵣ_eq
 
 example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
-    vecMul ![b₁, b₂] !![a₁₁, a₁₂; a₂₁, a₂₂] = ![b₁ * a₁₁ + b₂ * a₂₁, b₁ * a₁₂ + b₂ * a₂₂] :=
+    ![b₁, b₂] ᵥ* !![a₁₁, a₁₂; a₂₁, a₂₂] = ![b₁ * a₁₁ + b₂ * a₂₁, b₁ * a₁₂ + b₂ * a₂₂] :=
   (vecMulᵣ_eq _ _).symm
 
 /-- Expand `A` to `!![A 0 0, ...; ..., A m n]` -/
diff --git a/Mathlib/Data/Matrix/RowCol.lean b/Mathlib/Data/Matrix/RowCol.lean
index 8193c16eeeeff..5432d14b90e8f 100644
--- a/Mathlib/Data/Matrix/RowCol.lean
+++ b/Mathlib/Data/Matrix/RowCol.lean
@@ -115,25 +115,25 @@ theorem conjTranspose_row [Star α] (v : m → α) : (row v)ᴴ = col (star v) :
 #align matrix.conj_transpose_row Matrix.conjTranspose_row
 
 theorem row_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
-    Matrix.row (Matrix.vecMul v M) = Matrix.row v * M := by
+    Matrix.row (v ᵥ* M) = Matrix.row v * M := by
   ext
   rfl
 #align matrix.row_vec_mul Matrix.row_vecMul
 
 theorem col_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
-    Matrix.col (Matrix.vecMul v M) = (Matrix.row v * M)ᵀ := by
+    Matrix.col (v ᵥ* M) = (Matrix.row v * M)ᵀ := by
   ext
   rfl
 #align matrix.col_vec_mul Matrix.col_vecMul
 
 theorem col_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
-    Matrix.col (Matrix.mulVec M v) = M * Matrix.col v := by
+    Matrix.col (M *ᵥ v) = M * Matrix.col v := by
   ext
   rfl
 #align matrix.col_mul_vec Matrix.col_mulVec
 
 theorem row_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
-    Matrix.row (Matrix.mulVec M v) = (M * Matrix.col v)ᵀ := by
+    Matrix.row (M *ᵥ v) = (M * Matrix.col v)ᵀ := by
   ext
   rfl
 #align matrix.row_mul_vec Matrix.row_mulVec
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean b/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
index db448ff89f3f1..49843f14b3f1c 100644
--- a/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
+++ b/Mathlib/LinearAlgebra/AffineSpace/Matrix.lean
@@ -63,7 +63,7 @@ theorem affineIndependent_of_toMatrix_right_inv [DecidableEq ι'] (p : ι' → P
     (hA : b.toMatrix p * A = 1) : AffineIndependent k p := by
   rw [affineIndependent_iff_eq_of_fintype_affineCombination_eq]
   intro w₁ w₂ hw₁ hw₂ hweq
-  have hweq' : (b.toMatrix p).vecMul w₁ = (b.toMatrix p).vecMul w₂ := by
+  have hweq' : w₁ ᵥ* b.toMatrix p = w₂ ᵥ* b.toMatrix p := by
     ext j
     change (∑ i, w₁ i • b.coord j (p i)) = ∑ i, w₂ i • b.coord j (p i)
     -- Porting note: Added `u` because `∘` was causing trouble
@@ -72,7 +72,7 @@ theorem affineIndependent_of_toMatrix_right_inv [DecidableEq ι'] (p : ι' → P
       ← Finset.univ.affineCombination_eq_linear_combination _ _ hw₂, u,
       ← Finset.univ.map_affineCombination p w₁ hw₁, ← Finset.univ.map_affineCombination p w₂ hw₂,
       hweq]
-  replace hweq' := congr_arg (fun w => A.vecMul w) hweq'
+  replace hweq' := congr_arg (fun w => w ᵥ* A) hweq'
   simpa only [Matrix.vecMul_vecMul, hA, Matrix.vecMul_one] using hweq'
 #align affine_basis.affine_independent_of_to_matrix_right_inv AffineBasis.affineIndependent_of_toMatrix_right_inv
 
@@ -107,7 +107,7 @@ theorem affineSpan_eq_top_of_toMatrix_left_inv [DecidableEq ι] [Nontrivial k] (
 
 See also `AffineBasis.toMatrix_inv_vecMul_toMatrix`. -/
 @[simp]
-theorem toMatrix_vecMul_coords (x : P) : (b.toMatrix b₂).vecMul (b₂.coords x) = b.coords x := by
+theorem toMatrix_vecMul_coords (x : P) : b₂.coords x ᵥ* b.toMatrix b₂ = b.coords x := by
   ext j
   change _ = b.coord j x
   conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]
@@ -119,7 +119,7 @@ variable [DecidableEq ι]
 
 theorem toMatrix_mul_toMatrix : b.toMatrix b₂ * b₂.toMatrix b = 1 := by
   ext l m
-  change (b₂.toMatrix b).vecMul (b.coords (b₂ l)) m = _
+  change (b.coords (b₂ l) ᵥ* b₂.toMatrix b) m = _
   rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
 #align affine_basis.to_matrix_mul_to_matrix AffineBasis.toMatrix_mul_toMatrix
 
@@ -155,7 +155,7 @@ variable (b b₂ : AffineBasis ι k P)
 See also `AffineBasis.toMatrix_vecMul_coords`. -/
 @[simp]
 theorem toMatrix_inv_vecMul_toMatrix (x : P) :
-    (b.toMatrix b₂)⁻¹.vecMul (b.coords x) = b₂.coords x := by
+    b.coords x ᵥ* (b.toMatrix b₂)⁻¹ = b₂.coords x := by
   have hu := b.isUnit_toMatrix b₂
   rw [Matrix.isUnit_iff_isUnit_det] at hu
   rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
diff --git a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean
index a22097c3e9828..d05f37fa86817 100644
--- a/Mathlib/LinearAlgebra/Matrix/Adjugate.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Adjugate.lean
@@ -266,7 +266,7 @@ theorem adjugate_reindex (e : m ≃ n) (A : Matrix m m α) :
 /-- Since the map `b ↦ cramer A b` is linear in `b`, it must be multiplication by some matrix. This
 matrix is `A.adjugate`. -/
 theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) :
-    cramer A b = A.adjugate.mulVec b := by
+    cramer A b = A.adjugate *ᵥ b := by
   nth_rw 2 [← A.transpose_transpose]
   rw [← adjugate_transpose, adjugate_def]
   have : b = ∑ i, b i • Pi.single i 1 := by
@@ -309,7 +309,7 @@ theorem adjugate_smul (r : α) (A : Matrix n n α) :
 if the determinant is not a unit. A sufficient (but still not necessary) condition is that `A.det`
 divides `b`. -/
 @[simp]
-theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A.mulVec (cramer A b) = A.det • b := by
+theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b := by
   rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec_assoc, one_mulVec]
 #align matrix.mul_vec_cramer Matrix.mulVec_cramer
 
diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean
index e3aef3ab68d9c..cb527a3e1d4ff 100644
--- a/Mathlib/LinearAlgebra/Matrix/Basis.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean
@@ -126,7 +126,7 @@ theorem toMatrix_smul {R₁ S : Type*} [CommRing R₁] [Ring S] [Algebra R₁ S]
   rfl
 
 theorem toMatrix_map_vecMul {S : Type*} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S)
-    (v : ι' → S) : ((b.toMatrix v).map <| algebraMap R S).vecMul b = v := by
+    (v : ι' → S) : b ᵥ* ((b.toMatrix v).map <| algebraMap R S) = v := by
   ext i
   simp_rw [vecMul, dotProduct, Matrix.map_apply, ← Algebra.commutes, ← Algebra.smul_def,
     sum_toMatrix_smul_self]
diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
index a3df969451a62..3b5ff02491085 100644
--- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
+++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
@@ -139,7 +139,7 @@ theorem Matrix.toBilin'_apply (M : Matrix n n R₂) (x y : n → R₂) :
 #align matrix.to_bilin'_apply Matrix.toBilin'_apply
 
 theorem Matrix.toBilin'_apply' (M : Matrix n n R₂) (v w : n → R₂) :
-    Matrix.toBilin' M v w = Matrix.dotProduct v (M.mulVec w) := Matrix.toLinearMap₂'_apply' _ _ _
+    Matrix.toBilin' M v w = Matrix.dotProduct v (M *ᵥ w) := Matrix.toLinearMap₂'_apply' _ _ _
 #align matrix.to_bilin'_apply' Matrix.toBilin'_apply'
 
 @[simp]
diff --git a/Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean b/Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
index f11afc36fe559..c862c4d5861f9 100644
--- a/Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
@@ -29,7 +29,7 @@ variable {M : Type*} [AddCommGroup M] (R : Type*) [CommRing R] [Module R M] (I :
 
 variable (b : ι → M) (hb : Submodule.span R (Set.range b) = ⊤)
 
-open BigOperators Polynomial
+open BigOperators Polynomial Matrix
 
 /-- The composition of a matrix (as an endomorphism of `ι → R`) with the projection
 `(ι → R) →ₗ[R] M`.  -/
@@ -38,7 +38,7 @@ def PiToModule.fromMatrix [DecidableEq ι] : Matrix ι ι R →ₗ[R] (ι → R)
 #align pi_to_module.from_matrix PiToModule.fromMatrix
 
 theorem PiToModule.fromMatrix_apply [DecidableEq ι] (A : Matrix ι ι R) (w : ι → R) :
-    PiToModule.fromMatrix R b A w = Fintype.total R R b (A.mulVec w) :=
+    PiToModule.fromMatrix R b A w = Fintype.total R R b (A *ᵥ w) :=
   rfl
 #align pi_to_module.from_matrix_apply PiToModule.fromMatrix_apply
 
@@ -90,12 +90,12 @@ def Matrix.Represents (A : Matrix ι ι R) (f : Module.End R M) : Prop :=
 variable {b}
 
 theorem Matrix.Represents.congr_fun {A : Matrix ι ι R} {f : Module.End R M} (h : A.Represents b f)
-    (x) : Fintype.total R R b (A.mulVec x) = f (Fintype.total R R b x) :=
+    (x) : Fintype.total R R b (A *ᵥ x) = f (Fintype.total R R b x) :=
   LinearMap.congr_fun h x
 #align matrix.represents.congr_fun Matrix.Represents.congr_fun
 
 theorem Matrix.represents_iff {A : Matrix ι ι R} {f : Module.End R M} :
-    A.Represents b f ↔ ∀ x, Fintype.total R R b (A.mulVec x) = f (Fintype.total R R b x) :=
+    A.Represents b f ↔ ∀ x, Fintype.total R R b (A *ᵥ x) = f (Fintype.total R R b x) :=
   ⟨fun e x => e.congr_fun x, fun H => LinearMap.ext fun x => H x⟩
 #align matrix.represents_iff Matrix.represents_iff
 
diff --git a/Mathlib/LinearAlgebra/Matrix/Circulant.lean b/Mathlib/LinearAlgebra/Matrix/Circulant.lean
index 6f27198c5f261..033ba35e9bd6b 100644
--- a/Mathlib/LinearAlgebra/Matrix/Circulant.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Circulant.lean
@@ -18,7 +18,7 @@ Given a vector `v : n → α` indexed by a type that is endowed with subtraction
 
 - `Matrix.circulant`: the circulant matrix generated by a given vector `v : n → α`.
 - `Matrix.circulant_mul`: the product of two circulant matrices `circulant v` and `circulant w` is
-                          the circulant matrix generated by `mulVec (circulant v) w`.
+                          the circulant matrix generated by `circulant v *ᵥ w`.
 - `Matrix.circulant_mul_comm`: multiplication of circulant matrices commutes when the elements do.
 
 ## Implementation notes
@@ -121,9 +121,9 @@ theorem circulant_sub [Sub α] [Sub n] (v w : n → α) :
 #align matrix.circulant_sub Matrix.circulant_sub
 
 /-- The product of two circulant matrices `circulant v` and `circulant w` is
-    the circulant matrix generated by `mulVec (circulant v) w`. -/
+    the circulant matrix generated by `circulant v *ᵥ w`. -/
 theorem circulant_mul [Semiring α] [Fintype n] [AddGroup n] (v w : n → α) :
-    circulant v * circulant w = circulant (mulVec (circulant v) w) := by
+    circulant v * circulant w = circulant (circulant v *ᵥ w) := by
   ext i j
   simp only [mul_apply, mulVec, circulant_apply, dotProduct]
   refine' Fintype.sum_equiv (Equiv.subRight j) _ _ _
@@ -132,7 +132,7 @@ theorem circulant_mul [Semiring α] [Fintype n] [AddGroup n] (v w : n → α) :
 #align matrix.circulant_mul Matrix.circulant_mul
 
 theorem Fin.circulant_mul [Semiring α] :
-    ∀ {n} (v w : Fin n → α), circulant v * circulant w = circulant (mulVec (circulant v) w)
+    ∀ {n} (v w : Fin n → α), circulant v * circulant w = circulant (circulant v *ᵥ w)
   | 0 => by simp [Injective, eq_iff_true_of_subsingleton]
   | n + 1 => Matrix.circulant_mul
 #align matrix.fin.circulant_mul Matrix.Fin.circulant_mul
diff --git a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean
index 79e0829864147..d1f642920e7e8 100644
--- a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean
+++ b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean
@@ -148,21 +148,21 @@ lemma mul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (B : Matrix p n R) :
   simpa only [conjTranspose_conjTranspose] using mul_self_mul_conjTranspose_eq_zero Aᴴ _
 
 lemma conjTranspose_mul_self_mulVec_eq_zero (A : Matrix m n R) (v : n → R) :
-    (Aᴴ * A).mulVec v = 0 ↔ A.mulVec v = 0 := by
+    (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0 := by
   simpa only [← Matrix.col_mulVec, col_eq_zero] using
     conjTranspose_mul_self_mul_eq_zero A (col v)
 
 lemma self_mul_conjTranspose_mulVec_eq_zero (A : Matrix m n R) (v : m → R) :
-    (A * Aᴴ).mulVec v = 0 ↔ Aᴴ.mulVec v = 0 := by
+    (A * Aᴴ) *ᵥ v = 0 ↔ Aᴴ *ᵥ v = 0 := by
   simpa only [conjTranspose_conjTranspose] using conjTranspose_mul_self_mulVec_eq_zero Aᴴ _
 
 lemma vecMul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (v : n → R) :
-    vecMul v (Aᴴ * A) = 0 ↔ vecMul v Aᴴ = 0 := by
+    v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0 := by
   simpa only [← Matrix.row_vecMul, row_eq_zero] using
     mul_conjTranspose_mul_self_eq_zero A (row v)
 
 lemma vecMul_self_mul_conjTranspose_eq_zero (A : Matrix m n R) (v : m → R) :
-    vecMul v (A * Aᴴ) = 0 ↔ vecMul v A = 0 := by
+    v ᵥ* (A * Aᴴ) = 0 ↔ v ᵥ* A = 0 := by
   simpa only [conjTranspose_conjTranspose] using vecMul_conjTranspose_mul_self_eq_zero Aᴴ _
 
 end StarOrderedRing
diff --git a/Mathlib/LinearAlgebra/Matrix/LDL.lean b/Mathlib/LinearAlgebra/Matrix/LDL.lean
index a51759037605f..6e15e9be89557 100644
--- a/Mathlib/LinearAlgebra/Matrix/LDL.lean
+++ b/Mathlib/LinearAlgebra/Matrix/LDL.lean
@@ -77,13 +77,13 @@ noncomputable instance LDL.invertibleLowerInv : Invertible (LDL.lowerInv hS) :=
 #align LDL.invertible_lower_inv LDL.invertibleLowerInv
 
 theorem LDL.lowerInv_orthogonal {i j : n} (h₀ : i ≠ j) :
-    ⟪LDL.lowerInv hS i, Sᵀ.mulVec (LDL.lowerInv hS j)⟫ₑ = 0 :=
+    ⟪LDL.lowerInv hS i, Sᵀ *ᵥ LDL.lowerInv hS j⟫ₑ = 0 :=
   @gramSchmidt_orthogonal 𝕜 _ _ (_ : _) (InnerProductSpace.ofMatrix hS.transpose) _ _ _ _ _ _ _ h₀
 #align LDL.lower_inv_orthogonal LDL.lowerInv_orthogonal
 
 /-- The entries of the diagonal matrix `D` of the LDL decomposition. -/
 noncomputable def LDL.diagEntries : n → 𝕜 := fun i =>
-  ⟪star (LDL.lowerInv hS i), S.mulVec (star (LDL.lowerInv hS i))⟫ₑ
+  ⟪star (LDL.lowerInv hS i), S *ᵥ star (LDL.lowerInv hS i)⟫ₑ
 #align LDL.diag_entries LDL.diagEntries
 
 /-- The diagonal matrix `D` of the LDL decomposition. -/
diff --git a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
index adbb2d886d9de..dd38b1bfba96e 100644
--- a/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean
@@ -26,18 +26,18 @@ variable {m R A : Type*} [Fintype m] [CommRing R]
 
 /-- A matrix `M` is nondegenerate if for all `v ≠ 0`, there is a `w ≠ 0` with `w * M * v ≠ 0`. -/
 def Nondegenerate (M : Matrix m m R) :=
-  ∀ v, (∀ w, Matrix.dotProduct v (mulVec M w) = 0) → v = 0
+  ∀ v, (∀ w, Matrix.dotProduct v (M *ᵥ w) = 0) → v = 0
 #align matrix.nondegenerate Matrix.Nondegenerate
 
 /-- If `M` is nondegenerate and `w * M * v = 0` for all `w`, then `v = 0`. -/
 theorem Nondegenerate.eq_zero_of_ortho {M : Matrix m m R} (hM : Nondegenerate M) {v : m → R}
-    (hv : ∀ w, Matrix.dotProduct v (mulVec M w) = 0) : v = 0 :=
+    (hv : ∀ w, Matrix.dotProduct v (M *ᵥ w) = 0) : v = 0 :=
   hM v hv
 #align matrix.nondegenerate.eq_zero_of_ortho Matrix.Nondegenerate.eq_zero_of_ortho
 
 /-- If `M` is nondegenerate and `v ≠ 0`, then there is some `w` such that `w * M * v ≠ 0`. -/
 theorem Nondegenerate.exists_not_ortho_of_ne_zero {M : Matrix m m R} (hM : Nondegenerate M)
-    {v : m → R} (hv : v ≠ 0) : ∃ w, Matrix.dotProduct v (mulVec M w) ≠ 0 :=
+    {v : m → R} (hv : v ≠ 0) : ∃ w, Matrix.dotProduct v (M *ᵥ w) ≠ 0 :=
   not_forall.mp (mt hM.eq_zero_of_ortho hv)
 #align matrix.nondegenerate.exists_not_ortho_of_ne_zero Matrix.Nondegenerate.exists_not_ortho_of_ne_zero
 
@@ -64,13 +64,13 @@ theorem nondegenerate_of_det_ne_zero [DecidableEq m] {M : Matrix m m A} (hM : M.
 #align matrix.nondegenerate_of_det_ne_zero Matrix.nondegenerate_of_det_ne_zero
 
 theorem eq_zero_of_vecMul_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
-    (hv : M.vecMul v = 0) : v = 0 :=
+    (hv : v ᵥ* M = 0) : v = 0 :=
   (nondegenerate_of_det_ne_zero hM).eq_zero_of_ortho fun w => by
     rw [dotProduct_mulVec, hv, zero_dotProduct]
 #align matrix.eq_zero_of_vec_mul_eq_zero Matrix.eq_zero_of_vecMul_eq_zero
 
 theorem eq_zero_of_mulVec_eq_zero [DecidableEq m] {M : Matrix m m A} (hM : M.det ≠ 0) {v : m → A}
-    (hv : M.mulVec v = 0) : v = 0 :=
+    (hv : M *ᵥ v = 0) : v = 0 :=
   eq_zero_of_vecMul_eq_zero (by rwa [det_transpose]) ((vecMul_transpose M v).trans hv)
 #align matrix.eq_zero_of_mul_vec_eq_zero Matrix.eq_zero_of_mulVec_eq_zero
 
diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
index cad38b1541dac..fbc100feef745 100644
--- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
+++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
@@ -374,7 +374,7 @@ variable [Fintype m] [DecidableEq m] {K R : Type*} [Field K]
 
 theorem vecMul_surjective_iff_exists_left_inverse [Semiring R] {A : Matrix m n R} :
     Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by
-  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B.vecMul y, by simp [hBA]⟩⟩
+  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, by simp [hBA]⟩⟩
   choose rows hrows using (h <| Pi.single · 1)
   refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
   rw [mul_apply_eq_vecMul, one_eq_pi_single, ← hrows]
@@ -382,7 +382,7 @@ theorem vecMul_surjective_iff_exists_left_inverse [Semiring R] {A : Matrix m n R
 
 theorem mulVec_surjective_iff_exists_right_inverse [Semiring R] {A : Matrix m n R} :
     Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by
-  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B.mulVec y, by simp [hBA]⟩⟩
+  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
   choose cols hcols using (h <| Pi.single · 1)
   refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
   rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
@@ -667,7 +667,7 @@ theorem list_prod_inv_reverse : ∀ l : List (Matrix n n α), l.prod⁻¹ = (l.r
 /-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
 @[simp]
 theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
-    A.det • A⁻¹.mulVec b = cramer A b := by
+    A.det • A⁻¹ *ᵥ b = cramer A b := by
   rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec_assoc, smul_smul,
     h.mul_val_inv, one_smul]
 #align matrix.det_smul_inv_mul_vec_eq_cramer Matrix.det_smul_inv_mulVec_eq_cramer
@@ -675,7 +675,7 @@ theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : Is
 /-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
 @[simp]
 theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
-    A.det • A⁻¹.vecMul b = cramer Aᵀ b := by
+    A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by
   rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
     Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]
 #align matrix.det_smul_inv_vec_mul_eq_cramer_transpose Matrix.det_smul_inv_vecMul_eq_cramer_transpose
diff --git a/Mathlib/LinearAlgebra/Matrix/PosDef.lean b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
index bdc7c71d1a8d2..bb30598d8a0c2 100644
--- a/Mathlib/LinearAlgebra/Matrix/PosDef.lean
+++ b/Mathlib/LinearAlgebra/Matrix/PosDef.lean
@@ -45,7 +45,7 @@ open scoped Matrix
 /-- A matrix `M : Matrix n n R` is positive semidefinite if it is Hermitian and `xᴴ * M * x` is
 nonnegative for all `x`. -/
 def PosSemidef (M : Matrix n n R) :=
-  M.IsHermitian ∧ ∀ x : n → R, 0 ≤ dotProduct (star x) (M.mulVec x)
+  M.IsHermitian ∧ ∀ x : n → R, 0 ≤ dotProduct (star x) (M *ᵥ x)
 #align matrix.pos_semidef Matrix.PosSemidef
 
 /-- A diagonal matrix is positive semidefinite iff its diagonal entries are nonnegative. -/
@@ -62,7 +62,7 @@ theorem isHermitian {M : Matrix n n R} (hM : M.PosSemidef) : M.IsHermitian :=
   hM.1
 
 theorem re_dotProduct_nonneg {M : Matrix n n 𝕜} (hM : M.PosSemidef) (x : n → 𝕜) :
-    0 ≤ IsROrC.re (dotProduct (star x) (M.mulVec x)) :=
+    0 ≤ IsROrC.re (dotProduct (star x) (M *ᵥ x)) :=
   IsROrC.nonneg_iff.mp (hM.2 _) |>.1
 
 lemma conjTranspose_mul_mul_same {A : Matrix n n R} (hA : PosSemidef A)
@@ -71,7 +71,7 @@ lemma conjTranspose_mul_mul_same {A : Matrix n n R} (hA : PosSemidef A)
   constructor
   · exact isHermitian_conjTranspose_mul_mul B hA.1
   · intro x
-    simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.2 (mulVec B x)
+    simpa only [star_mulVec, dotProduct_mulVec, vecMul_vecMul] using hA.2 (B *ᵥ x)
 
 lemma mul_mul_conjTranspose_same {A : Matrix n n R} (hA : PosSemidef A)
     {m : Type*} [Fintype m] (B : Matrix m n R):
@@ -198,29 +198,29 @@ lemma eq_of_sq_eq_sq {B : Matrix n n 𝕜} (hB : PosSemidef B) (hAB : A ^ 2 = B
   `⟨v, (A - B) v⟩ = 0`, but this is a nonzero scalar multiple of `⟨v, v⟩`, contradiction. -/
   by_contra h_ne
   let ⟨v, t, ht, hv, hv'⟩ := (hA.1.sub hB.1).exists_eigenvector_of_ne_zero (sub_ne_zero.mpr h_ne)
-  have h_sum : 0 = t * (star v ⬝ᵥ mulVec A v + star v ⬝ᵥ mulVec B v)
+  have h_sum : 0 = t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v)
   · calc
-      0 = star v ⬝ᵥ mulVec (A ^ 2 - B ^ 2) v := by rw [hAB, sub_self, zero_mulVec, dotProduct_zero]
-      _ = star v ⬝ᵥ mulVec A (mulVec (A - B) v)  + star v ⬝ᵥ mulVec (A - B) (mulVec B v) := by
+      0 = star v ⬝ᵥ (A ^ 2 - B ^ 2) *ᵥ v := by rw [hAB, sub_self, zero_mulVec, dotProduct_zero]
+      _ = star v ⬝ᵥ A *ᵥ (A - B) *ᵥ v + star v ⬝ᵥ (A - B) *ᵥ B *ᵥ v := by
         rw [mulVec_mulVec, mulVec_mulVec, ← dotProduct_add, ← add_mulVec, mul_sub, sub_mul,
           add_sub, sub_add_cancel, pow_two, pow_two]
-      _ = t * (star v ⬝ᵥ mulVec A v) + vecMul (star v) (A - B)ᴴ ⬝ᵥ mulVec B v := by
+      _ = t * (star v ⬝ᵥ A *ᵥ v) + (star v) ᵥ* (A - B)ᴴ ⬝ᵥ B *ᵥ v := by
         rw [hv', mulVec_smul, dotProduct_smul, IsROrC.real_smul_eq_coe_mul,
           dotProduct_mulVec _ (A - B), hA.1.sub hB.1]
-      _ = t * (star v ⬝ᵥ mulVec A v + star v ⬝ᵥ mulVec B v) := by
+      _ = t * (star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v) := by
         simp_rw [← star_mulVec, hv', mul_add, ← IsROrC.real_smul_eq_coe_mul, ← smul_dotProduct]
         congr 2 with i
         simp only [Pi.star_apply, Pi.smul_apply, IsROrC.real_smul_eq_coe_mul, star_mul',
           IsROrC.star_def, IsROrC.conj_ofReal]
-  replace h_sum : star v ⬝ᵥ mulVec A v + star v ⬝ᵥ mulVec B v = 0
+  replace h_sum : star v ⬝ᵥ A *ᵥ v + star v ⬝ᵥ B *ᵥ v = 0
   · rw [eq_comm, ← mul_zero (t : 𝕜)] at h_sum
     exact mul_left_cancel₀ (IsROrC.ofReal_ne_zero.mpr ht) h_sum
-  have h_van : star v ⬝ᵥ mulVec A v = 0 ∧ star v ⬝ᵥ mulVec B v = 0
+  have h_van : star v ⬝ᵥ A *ᵥ v = 0 ∧ star v ⬝ᵥ B *ᵥ v = 0
   · refine ⟨le_antisymm ?_ (hA.2 v), le_antisymm ?_ (hB.2 v)⟩
     · rw [add_comm, add_eq_zero_iff_eq_neg] at h_sum
       simpa only [h_sum, neg_nonneg] using hB.2 v
     · simpa only [add_eq_zero_iff_eq_neg.mp h_sum, neg_nonneg] using hA.2 v
-  have aux : star v ⬝ᵥ mulVec (A - B) v = 0
+  have aux : star v ⬝ᵥ (A - B) *ᵥ v = 0
   · rw [sub_mulVec, dotProduct_sub, h_van.1, h_van.2, sub_zero]
   rw [hv', dotProduct_smul, IsROrC.real_smul_eq_coe_mul, ← mul_zero ↑t] at aux
   exact hv <| Matrix.dotProduct_star_self_eq_zero.mp <| mul_left_cancel₀
@@ -279,7 +279,7 @@ lemma IsHermitian.posSemidef_of_eigenvalues_nonneg [DecidableEq n] {A : Matrix n
 /-- For `A` positive semidefinite, we have `x⋆ A x = 0` iff `A x = 0`. -/
 theorem PosSemidef.dotProduct_mulVec_zero_iff
     {A : Matrix n n 𝕜} (hA : PosSemidef A) (x : n → 𝕜) :
-    star x ⬝ᵥ mulVec A x = 0 ↔ mulVec A x = 0 := by
+    star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0 := by
   constructor
   · obtain ⟨B, rfl⟩ := posSemidef_iff_eq_transpose_mul_self.mp hA
     rw [← Matrix.mulVec_mulVec, dotProduct_mulVec,
@@ -302,7 +302,7 @@ theorem PosSemidef.toLinearMap₂'_zero_iff [DecidableEq n]
 /-- A matrix `M : Matrix n n R` is positive definite if it is hermitian
    and `xᴴMx` is greater than zero for all nonzero `x`. -/
 def PosDef (M : Matrix n n R) :=
-  M.IsHermitian ∧ ∀ x : n → R, x ≠ 0 → 0 < dotProduct (star x) (M.mulVec x)
+  M.IsHermitian ∧ ∀ x : n → R, x ≠ 0 → 0 < dotProduct (star x) (M *ᵥ x)
 #align matrix.pos_def Matrix.PosDef
 
 namespace PosDef
@@ -312,7 +312,7 @@ theorem isHermitian {M : Matrix n n R} (hM : M.PosDef) : M.IsHermitian :=
 #align matrix.pos_def.is_hermitian Matrix.PosDef.isHermitian
 
 theorem re_dotProduct_pos {M : Matrix n n 𝕜} (hM : M.PosDef) {x : n → 𝕜} (hx : x ≠ 0) :
-    0 < IsROrC.re (dotProduct (star x) (M.mulVec x)) :=
+    0 < IsROrC.re (dotProduct (star x) (M *ᵥ x)) :=
   IsROrC.pos_iff.mp (hM.2 _ hx) |>.1
 
 theorem posSemidef {M : Matrix n n R} (hM : M.PosDef) : M.PosSemidef := by
@@ -396,7 +396,7 @@ variable {𝕜 : Type*} [IsROrC 𝕜] {n : Type*} [Fintype n]
 noncomputable def NormedAddCommGroup.ofMatrix {M : Matrix n n 𝕜} (hM : M.PosDef) :
     NormedAddCommGroup (n → 𝕜) :=
   @InnerProductSpace.Core.toNormedAddCommGroup _ _ _ _ _
-    { inner := fun x y => dotProduct (star x) (M.mulVec y)
+    { inner := fun x y => dotProduct (star x) (M *ᵥ y)
       conj_symm := fun x y => by
         dsimp only [Inner.inner]
         rw [star_dotProduct, starRingEnd_apply, star_star, star_mulVec, dotProduct_mulVec,
diff --git a/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean b/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
index bef83b3a72173..eba57fc328cd2 100644
--- a/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
+++ b/Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
@@ -453,7 +453,7 @@ theorem det_one_add_col_mul_row (u v : m → α) : det (1 + col u * row v) = 1 +
 /-- The **Matrix determinant lemma**
 
 TODO: show the more general version without `hA : IsUnit A.det` as
-`(A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A).mulVec u`.
+`(A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u`.
 -/
 theorem det_add_col_mul_row {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :
     (A + col u * row v).det = A.det * (1 + row v * A⁻¹ * col u).det := by
@@ -486,9 +486,9 @@ scoped infixl:65 " ⊕ᵥ " => Sum.elim
 theorem schur_complement_eq₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜}
     (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (x : m → 𝕜) (y : n → 𝕜) [Invertible A]
     (hA : A.IsHermitian) :
-    vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
-      vecMul (star (x + (A⁻¹ * B).mulVec y)) A ⬝ᵥ (x + (A⁻¹ * B).mulVec y) +
-        vecMul (star y) (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y := by
+    (star (x ⊕ᵥ y)) ᵥ* (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
+      (star (x + (A⁻¹ * B) *ᵥ y)) ᵥ* A ⬝ᵥ (x + (A⁻¹ * B) *ᵥ y) +
+        (star y) ᵥ* (D - Bᴴ * A⁻¹ * B) ⬝ᵥ y := by
   simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
     dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hA.eq,
     conjTranspose_nonsing_inv, star_mulVec]
@@ -498,9 +498,9 @@ theorem schur_complement_eq₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A : M
 theorem schur_complement_eq₂₂ [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜)
     (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (x : m → 𝕜) (y : n → 𝕜) [Invertible D]
     (hD : D.IsHermitian) :
-    vecMul (star (x ⊕ᵥ y)) (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
-      vecMul (star ((D⁻¹ * Bᴴ).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * Bᴴ).mulVec x + y) +
-        vecMul (star x) (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x := by
+    (star (x ⊕ᵥ y)) ᵥ* (fromBlocks A B Bᴴ D) ⬝ᵥ (x ⊕ᵥ y) =
+      (star ((D⁻¹ * Bᴴ) *ᵥ x + y)) ᵥ* D ⬝ᵥ ((D⁻¹ * Bᴴ) *ᵥ x + y) +
+        (star x) ᵥ* (A - B * D⁻¹ * Bᴴ) ⬝ᵥ x := by
   simp [Function.star_sum_elim, fromBlocks_mulVec, vecMul_fromBlocks, add_vecMul,
     dotProduct_mulVec, vecMul_sub, Matrix.mul_assoc, vecMul_mulVec, hD.eq,
     conjTranspose_nonsing_inv, star_mulVec]
@@ -537,7 +537,7 @@ theorem PosSemidef.fromBlocks₁₁ [Fintype m] [DecidableEq m] [Fintype n] {A :
   rw [PosSemidef, IsHermitian.fromBlocks₁₁ _ _ hA.1]
   constructor
   · refine' fun h => ⟨h.1, fun x => _⟩
-    have := h.2 (-(A⁻¹ * B).mulVec x ⊕ᵥ x)
+    have := h.2 (-((A⁻¹ * B) *ᵥ x) ⊕ᵥ x)
     rw [dotProduct_mulVec, schur_complement_eq₁₁ B D _ _ hA.1, neg_add_self, dotProduct_zero,
       zero_add] at this
     rw [dotProduct_mulVec]; exact this
diff --git a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
index 118ed4872458c..87ddb9e251ed0 100644
--- a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
+++ b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
@@ -205,7 +205,7 @@ theorem Matrix.toLinearMap₂'_apply (M : Matrix n m R) (x : n → R) (y : m →
 #align matrix.to_linear_map₂'_apply Matrix.toLinearMap₂'_apply
 
 theorem Matrix.toLinearMap₂'_apply' (M : Matrix n m R) (v : n → R) (w : m → R) :
-    Matrix.toLinearMap₂' M v w = Matrix.dotProduct v (M.mulVec w) := by
+    Matrix.toLinearMap₂' M v w = Matrix.dotProduct v (M *ᵥ w) := by
   simp_rw [Matrix.toLinearMap₂'_apply, Matrix.dotProduct, Matrix.mulVec, Matrix.dotProduct]
   refine' Finset.sum_congr rfl fun _ _ => _
   rw [Finset.mul_sum]
diff --git a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
index 5b9af045df48b..3c6b776b4012e 100644
--- a/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
+++ b/Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
@@ -382,7 +382,7 @@ lemma exists_SL2_row {a b : R} (hab : IsCoprime a b) (i : Fin 2):
 /-- A vector with coprime entries, right-multiplied by a matrix in `SL(2, R)`, has
 coprime entries. -/
 lemma vecMulSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
-    IsCoprime (vecMul v A.1 0) (vecMul v A.1 1) := by
+    IsCoprime ((v ᵥ* A.1) 0) ((v ᵥ* A.1) 1) := by
   obtain ⟨g, hg⟩ := hab.exists_SL2_row 0
   have : v = g 0 := funext fun t ↦ by { fin_cases t <;> tauto }
   simpa only [this] using isCoprime_row (g * A) 0
@@ -390,7 +390,7 @@ lemma vecMulSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
 /-- A vector with coprime entries, left-multiplied by a matrix in `SL(2, R)`, has
 coprime entries. -/
 lemma mulVecSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
-    IsCoprime (mulVec A.1 v 0) (mulVec A.1 v 1) := by
+    IsCoprime ((A.1 *ᵥ v) 0) ((A.1 *ᵥ v) 1) := by
   simpa only [← vecMul_transpose] using hab.vecMulSL A.transpose
 
 end IsCoprime
diff --git a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
index 334b7548535da..c25a5c802b1b0 100644
--- a/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
+++ b/Mathlib/LinearAlgebra/Matrix/Spectrum.lean
@@ -125,7 +125,7 @@ theorem spectral_theorem :
 
 theorem eigenvalues_eq (i : n) :
     hA.eigenvalues i =
-      IsROrC.re (star (hA.eigenvectorMatrixᵀ i) ⬝ᵥ A.mulVec (hA.eigenvectorMatrixᵀ i)) := by
+      IsROrC.re (star (hA.eigenvectorMatrixᵀ i) ⬝ᵥ A *ᵥ hA.eigenvectorMatrixᵀ i) := by
   have := hA.spectral_theorem
   rw [← @Matrix.mul_inv_eq_iff_eq_mul_of_invertible (A := hA.eigenvectorMatrixInv)] at this
   have := congr_arg IsROrC.re (congr_fun (congr_fun this i) i)
@@ -165,7 +165,7 @@ lemma rank_eq_card_non_zero_eigs : A.rank = Fintype.card {i // hA.eigenvalues i
 
 /-- The entries of `eigenvectorBasis` are eigenvectors. -/
 lemma mulVec_eigenvectorBasis (i : n) :
-    mulVec A (hA.eigenvectorBasis i) = hA.eigenvalues i • hA.eigenvectorBasis i := by
+    A *ᵥ hA.eigenvectorBasis i = hA.eigenvalues i • hA.eigenvectorBasis i := by
   have := congr_arg (· * hA.eigenvectorMatrix) hA.spectral_theorem'
   simp only [mul_assoc, mul_eq_one_comm.mp hA.eigenvectorMatrix_mul_inv, mul_one] at this
   ext1 j
@@ -178,7 +178,7 @@ end DecidableEq
 
 /-- A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue. -/
 lemma exists_eigenvector_of_ne_zero (hA : IsHermitian A) (h_ne : A ≠ 0) :
-    ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ mulVec A v = t • v := by
+    ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A *ᵥ v = t • v := by
   classical
   have : hA.eigenvalues ≠ 0
   · contrapose! h_ne
diff --git a/Mathlib/LinearAlgebra/Matrix/ToLin.lean b/Mathlib/LinearAlgebra/Matrix/ToLin.lean
index 93d38bdb8fb2f..8b912532ca588 100644
--- a/Mathlib/LinearAlgebra/Matrix/ToLin.lean
+++ b/Mathlib/LinearAlgebra/Matrix/ToLin.lean
@@ -84,13 +84,13 @@ variable {l m n : Type*}
 
 /-- `Matrix.vecMul M` is a linear map. -/
 def Matrix.vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R where
-  toFun x := M.vecMul x
+  toFun x := x ᵥ* M
   map_add' _ _ := funext fun _ => add_dotProduct _ _ _
   map_smul' _ _ := funext fun _ => smul_dotProduct _ _ _
 #align matrix.vec_mul_linear Matrix.vecMulLinear
 
 @[simp] theorem Matrix.vecMulLinear_apply [Fintype m] (M : Matrix m n R) (x : m → R) :
-    M.vecMulLinear x = M.vecMul x := rfl
+    M.vecMulLinear x = x ᵥ* M := rfl
 
 theorem Matrix.coe_vecMulLinear [Fintype m] (M : Matrix m n R) :
     (M.vecMulLinear : _ → _) = M.vecMul := rfl
@@ -99,7 +99,7 @@ variable [Fintype m] [DecidableEq m]
 
 @[simp]
 theorem Matrix.vecMul_stdBasis (M : Matrix m n R) (i j) :
-    M.vecMul (LinearMap.stdBasis R (fun _ => R) i 1) j = M i j := by
+    (LinearMap.stdBasis R (fun _ => R) i 1 ᵥ* M) j = M i j := by
   have : (∑ i', (if i = i' then 1 else 0) * M i' j) = M i j := by
     simp_rw [boole_mul, Finset.sum_ite_eq, Finset.mem_univ, if_true]
   simp only [vecMul, dotProduct]
@@ -162,7 +162,7 @@ abbrev Matrix.toLinearMapRight' : Matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →
 @[simp]
 theorem Matrix.toLinearMapRight'_apply (M : Matrix m n R) (v : m → R) :
     -- porting note: needs type annotation for `⇑` to resolve
-    (Matrix.toLinearMapRight' : _ ≃ₗ[Rᵐᵒᵖ] _) M v = M.vecMul v :=
+    (Matrix.toLinearMapRight' : _ ≃ₗ[Rᵐᵒᵖ] _) M v = v ᵥ* M :=
   rfl
 #align matrix.to_linear_map_right'_apply Matrix.toLinearMapRight'_apply
 
@@ -240,7 +240,7 @@ theorem Matrix.coe_mulVecLin [Fintype n] (M : Matrix m n R) :
 
 @[simp]
 theorem Matrix.mulVecLin_apply [Fintype n] (M : Matrix m n R) (v : n → R) :
-    M.mulVecLin v = M.mulVec v :=
+    M.mulVecLin v = M *ᵥ v :=
   rfl
 #align matrix.mul_vec_lin_apply Matrix.mulVecLin_apply
 
@@ -293,18 +293,18 @@ theorem Matrix.mulVecLin_mul [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
 #align matrix.mul_vec_lin_mul Matrix.mulVecLin_mul
 
 theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
-    (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M.mulVec v = 0 → v = 0 := by
+    (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 := by
   simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]
 #align matrix.ker_mul_vec_lin_eq_bot_iff Matrix.ker_mulVecLin_eq_bot_iff
 
 theorem Matrix.mulVec_stdBasis [DecidableEq n] (M : Matrix m n R) (i j) :
-    M.mulVec (LinearMap.stdBasis R (fun _ => R) j 1) i = M i j :=
+    (M *ᵥ LinearMap.stdBasis R (fun _ => R) j 1) i = M i j :=
   (congr_fun (Matrix.mulVec_single _ _ (1 : R)) i).trans <| mul_one _
 #align matrix.mul_vec_std_basis Matrix.mulVec_stdBasis
 
 @[simp]
 theorem Matrix.mulVec_stdBasis_apply [DecidableEq n] (M : Matrix m n R) (j) :
-    M.mulVec (LinearMap.stdBasis R (fun _ => R) j 1) = Mᵀ j :=
+    M *ᵥ LinearMap.stdBasis R (fun _ => R) j 1 = Mᵀ j :=
   funext fun i => Matrix.mulVec_stdBasis M i j
 #align matrix.mul_vec_std_basis_apply Matrix.mulVec_stdBasis_apply
 
@@ -392,7 +392,7 @@ theorem LinearMap.toMatrix'_apply (f : (n → R) →ₗ[R] m → R) (i j) :
 #align linear_map.to_matrix'_apply LinearMap.toMatrix'_apply
 
 @[simp]
-theorem Matrix.toLin'_apply (M : Matrix m n R) (v : n → R) : Matrix.toLin' M v = M.mulVec v :=
+theorem Matrix.toLin'_apply (M : Matrix m n R) (v : n → R) : Matrix.toLin' M v = M *ᵥ v :=
   rfl
 #align matrix.to_lin'_apply Matrix.toLin'_apply
 
@@ -460,7 +460,7 @@ theorem LinearMap.toMatrix'_algebraMap (x : R) :
 #align linear_map.to_matrix'_algebra_map LinearMap.toMatrix'_algebraMap
 
 theorem Matrix.ker_toLin'_eq_bot_iff {M : Matrix n n R} :
-    LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ v, M.mulVec v = 0 → v = 0 :=
+    LinearMap.ker (Matrix.toLin' M) = ⊥ ↔ ∀ v, M *ᵥ v = 0 → v = 0 :=
   Matrix.ker_mulVecLin_eq_bot_iff
 #align matrix.ker_to_lin'_eq_bot_iff Matrix.ker_toLin'_eq_bot_iff
 
@@ -525,7 +525,7 @@ theorem LinearMap.toMatrixAlgEquiv'_apply (f : (n → R) →ₗ[R] n → R) (i j
 
 @[simp]
 theorem Matrix.toLinAlgEquiv'_apply (M : Matrix n n R) (v : n → R) :
-    Matrix.toLinAlgEquiv' M v = M.mulVec v :=
+    Matrix.toLinAlgEquiv' M v = M *ᵥ v :=
   rfl
 #align matrix.to_lin_alg_equiv'_apply Matrix.toLinAlgEquiv'_apply
 
@@ -643,7 +643,7 @@ theorem LinearMap.toMatrix_transpose_apply' (f : M₁ →ₗ[R] M₂) (j : n) :
 #align linear_map.to_matrix_transpose_apply' LinearMap.toMatrix_transpose_apply'
 
 theorem Matrix.toLin_apply (M : Matrix m n R) (v : M₁) :
-    Matrix.toLin v₁ v₂ M v = ∑ j, M.mulVec (v₁.repr v) j • v₂ j :=
+    Matrix.toLin v₁ v₂ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₂ j :=
   show v₂.equivFun.symm (Matrix.toLin' M (v₁.repr v)) = _ by
     rw [Matrix.toLin'_apply, v₂.equivFun_symm_apply]
 #align matrix.to_lin_apply Matrix.toLin_apply
@@ -711,7 +711,7 @@ theorem LinearMap.toMatrix_algebraMap (x : R) :
 #align linear_map.to_matrix_algebra_map LinearMap.toMatrix_algebraMap
 
 theorem LinearMap.toMatrix_mulVec_repr (f : M₁ →ₗ[R] M₂) (x : M₁) :
-    (LinearMap.toMatrix v₁ v₂ f).mulVec (v₁.repr x) = v₂.repr (f x) := by
+    LinearMap.toMatrix v₁ v₂ f *ᵥ v₁.repr x = v₂.repr (f x) := by
   ext i
   rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
     LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
@@ -813,7 +813,7 @@ theorem LinearMap.toMatrixAlgEquiv_transpose_apply' (f : M₁ →ₗ[R] M₁) (j
 #align linear_map.to_matrix_alg_equiv_transpose_apply' LinearMap.toMatrixAlgEquiv_transpose_apply'
 
 theorem Matrix.toLinAlgEquiv_apply (M : Matrix n n R) (v : M₁) :
-    Matrix.toLinAlgEquiv v₁ M v = ∑ j, M.mulVec (v₁.repr v) j • v₁ j :=
+    Matrix.toLinAlgEquiv v₁ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₁ j :=
   show v₁.equivFun.symm (Matrix.toLinAlgEquiv' M (v₁.repr v)) = _ by
     rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]
 #align matrix.to_lin_alg_equiv_apply Matrix.toLinAlgEquiv_apply
@@ -945,7 +945,7 @@ theorem leftMulMatrix_eq_repr_mul (x : S) (i j) : leftMulMatrix b x i j = b.repr
 #align algebra.left_mul_matrix_eq_repr_mul Algebra.leftMulMatrix_eq_repr_mul
 
 theorem leftMulMatrix_mulVec_repr (x y : S) :
-    (leftMulMatrix b x).mulVec (b.repr y) = b.repr (x * y) :=
+    leftMulMatrix b x *ᵥ b.repr y = b.repr (x * y) :=
   (LinearMap.mulLeft R x).toMatrix_mulVec_repr b b y
 #align algebra.left_mul_matrix_mul_vec_repr Algebra.leftMulMatrix_mulVec_repr
 
diff --git a/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean b/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
index 9af7edba13e7a..f80badd72916a 100644
--- a/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
+++ b/Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean
@@ -113,7 +113,7 @@ open Matrix
 /-- This holds for all integral domains (see `Matrix.exists_mulVec_eq_zero_iff`),
 not just fields, but it's easier to prove it for the field of fractions first. -/
 theorem exists_mulVec_eq_zero_iff_aux {K : Type*} [DecidableEq n] [Field K] {M : Matrix n n K} :
-    (∃ v ≠ 0, M.mulVec v = 0) ↔ M.det = 0 := by
+    (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 := by
   constructor
   · rintro ⟨v, hv, mul_eq⟩
     contrapose! hv
@@ -135,8 +135,8 @@ theorem exists_mulVec_eq_zero_iff_aux {K : Type*} [DecidableEq n] [Field K] {M :
 
 theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [CommRing A]
     [Nontrivial A] [Field K] [Algebra A K] [IsFractionRing A K] {M : Matrix n n A} :
-    (∃ v ≠ 0, M.mulVec v = 0) ↔ M.det = 0 := by
-  have : (∃ v ≠ 0, mulVec ((algebraMap A K).mapMatrix M) v = 0) ↔ _ :=
+    (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 := by
+  have : (∃ v ≠ 0, (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ _ :=
     exists_mulVec_eq_zero_iff_aux
   rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this
   refine' Iff.trans _ this; constructor <;> rintro ⟨v, hv, mul_eq⟩
@@ -159,8 +159,8 @@ theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [Comm
     · ext i
       refine' IsFractionRing.injective A K _
       calc
-        algebraMap A K (M.mulVec (fun i : n => f (v i) _) i) =
-            ((algebraMap A K).mapMatrix M).mulVec (algebraMap _ K b • v) i := ?_
+        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
+            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
         _ = 0 := ?_
         _ = algebraMap A K 0 := (RingHom.map_zero _).symm
       · simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
@@ -169,12 +169,12 @@ theorem exists_mulVec_eq_zero_iff' {A : Type*} (K : Type*) [DecidableEq n] [Comm
 #align matrix.exists_mul_vec_eq_zero_iff' Matrix.exists_mulVec_eq_zero_iff'
 
 theorem exists_mulVec_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : (∃ v ≠ 0, M.mulVec v = 0) ↔ M.det = 0 :=
+    {M : Matrix n n A} : (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 :=
   exists_mulVec_eq_zero_iff' (FractionRing A)
 #align matrix.exists_mul_vec_eq_zero_iff Matrix.exists_mulVec_eq_zero_iff
 
 theorem exists_vecMul_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A]
-    {M : Matrix n n A} : (∃ v ≠ 0, M.vecMul v = 0) ↔ M.det = 0 := by
+    {M : Matrix n n A} : (∃ v ≠ 0, v ᵥ* M = 0) ↔ M.det = 0 := by
   simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff
 #align matrix.exists_vec_mul_eq_zero_iff Matrix.exists_vecMul_eq_zero_iff
 
diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
index ed94627cb7fb7..242d34a6eafcb 100644
--- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
+++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Basic.lean
@@ -58,9 +58,9 @@ variable {N a}
 
 section gamma_action
 
-/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (vecMul a γ)`. -/
+/-- Right-multiplying by `γ ∈ SL(2, ℤ)` sends `gammaSet N a` to `gammaSet N (a ᵥ* γ)`. -/
 lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ : SL(2, ℤ)) :
-    vecMul v γ ∈ gammaSet N (vecMul a γ) := by
+    v ᵥ* γ ∈ gammaSet N (a ᵥ* γ) := by
   refine ⟨?_, hv.2.vecMulSL γ⟩
   have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
   simp only [eq_intCast, Int.coe_castRingHom] at this
@@ -69,9 +69,9 @@ lemma vecMul_SL2_mem_gammaSet {v : Fin 2 → ℤ} (hv : v ∈ gammaSet N a) (γ
 
 variable (a) in
 /-- The bijection between `GammaSets` given by multiplying by an element of `SL(2, ℤ)`. -/
-def gammaSetEquiv (γ : SL(2, ℤ)) : gammaSet N a ≃ gammaSet N (vecMul a γ) where
-  toFun v := ⟨vecMul v.1 γ, vecMul_SL2_mem_gammaSet v.2 γ⟩
-  invFun v := ⟨vecMul v.1 ↑(γ⁻¹), by
+def gammaSetEquiv (γ : SL(2, ℤ)) : gammaSet N a ≃ gammaSet N (a ᵥ* γ) where
+  toFun v := ⟨v.1 ᵥ* γ, vecMul_SL2_mem_gammaSet v.2 γ⟩
+  invFun v := ⟨v.1 ᵥ* ↑(γ⁻¹), by
       have := vecMul_SL2_mem_gammaSet v.2 γ⁻¹
       rw [vecMul_vecMul, ← SpecialLinearGroup.coe_mul] at this
       simpa only [SpecialLinearGroup.map_apply_coe, RingHom.mapMatrix_apply, Int.coe_castRingHom,
@@ -90,7 +90,7 @@ def eisSummand (k : ℤ) (v : Fin 2 → ℤ) (z : ℍ) : ℂ := 1 / (v 0 * z.1 +
 
 /-- How the `eisSummand` function changes under the Moebius action. -/
 theorem eisSummand_SL2_apply (k : ℤ) (i : (Fin 2 → ℤ)) (A : SL(2, ℤ)) (z : ℍ) :
-    eisSummand k i (A • z) = (z.denom A) ^ k * eisSummand k (vecMul i A) z := by
+    eisSummand k i (A • z) = (z.denom A) ^ k * eisSummand k (i ᵥ* A) z := by
   simp only [eisSummand, specialLinearGroup_apply, algebraMap_int_eq, eq_intCast, ofReal_int_cast,
     one_div, vecMul, vec2_dotProduct, Int.cast_add, Int.cast_mul]
   have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : ((u * ((a * z + b) / (c * z + d)) + v) ^ k)⁻¹ =
@@ -107,7 +107,7 @@ variable (a)
 def eisensteinSeries (k : ℤ) (z : ℍ) : ℂ := ∑' x : gammaSet N a, eisSummand k x z
 
 lemma eisensteinSeries_slash_apply (k : ℤ) (γ : SL(2, ℤ)) :
-    eisensteinSeries a k ∣[k] γ = eisensteinSeries (vecMul a γ) k := by
+    eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* γ) k := by
   ext1 z
   simp_rw [SL_slash, slash_def, slash, det_coe', ofReal_one, one_zpow, mul_one, zpow_neg,
     mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| z.denom_ne_zero _), mul_comm,
diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
index 56d18bcc4db37..0584d4d27bb42 100644
--- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
+++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean
@@ -357,7 +357,7 @@ representation of `commMap K x` on `stdBasis` is given (up to reindexing) by the
 theorem stdBasis_repr_eq_matrixToStdBasis_mul (x : (K →+* ℂ) → ℂ)
     (hx : ∀ φ, conj (x φ) = x (ComplexEmbedding.conjugate φ)) (c : index K) :
     ((stdBasis K).repr (commMap K x) c : ℂ) =
-      (mulVec (matrixToStdBasis K) (x ∘ (indexEquiv K))) c := by
+      (matrixToStdBasis K *ᵥ (x ∘ (indexEquiv K))) c := by
   simp_rw [commMap, matrixToStdBasis, LinearMap.coe_mk, AddHom.coe_mk,
     mulVec, dotProduct, Function.comp_apply, index, Fintype.sum_sum_type,
     diagonal_one, reindex_apply, ← Finset.univ_product_univ, Finset.sum_product,
diff --git a/Mathlib/RingTheory/Discriminant.lean b/Mathlib/RingTheory/Discriminant.lean
index bcce983e92ff8..94c468526bc10 100644
--- a/Mathlib/RingTheory/Discriminant.lean
+++ b/Mathlib/RingTheory/Discriminant.lean
@@ -25,8 +25,8 @@ Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we
 * `Algebra.discr_zero_of_not_linearIndependent` : if `b` is not linear independent, then
   `Algebra.discr A b = 0`.
 * `Algebra.discr_of_matrix_vecMul` and `Algebra.discr_of_matrix_mulVec` : formulas relating
-  `Algebra.discr A ι b` with `Algebra.discr A ((P.map (algebraMap A B)).vecMul b)` and
-  `Algebra.discr A ((P.map (algebraMap A B)).mulVec b)`.
+  `Algebra.discr A ι b` with `Algebra.discr A (b ᵥ* P.map (algebraMap A B))` and
+  `Algebra.discr A (P.map (algebraMap A B) *ᵥ b)`.
 * `Algebra.discr_not_zero_of_basis` : over a field, if `b` is a basis, then
   `Algebra.discr K b ≠ 0`.
 * `Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two` : if `L/K` is a field extension and
@@ -98,7 +98,7 @@ theorem discr_zero_of_not_linearIndependent [IsDomain A] {b : ι → B}
     (hli : ¬LinearIndependent A b) : discr A b = 0 := by
   classical
   obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
-  have : (traceMatrix A b).mulVec g = 0 := by
+  have : (traceMatrix A b) *ᵥ g = 0 := by
     ext i
     have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by
       intro j;
@@ -113,17 +113,17 @@ theorem discr_zero_of_not_linearIndependent [IsDomain A] {b : ι → B}
 variable {A}
 
 /-- Relation between `Algebra.discr A ι b` and
-`Algebra.discr A ((P.map (algebraMap A B)).vecMul b)`. -/
+`Algebra.discr A (b ᵥ* P.map (algebraMap A B))`. -/
 theorem discr_of_matrix_vecMul (b : ι → B) (P : Matrix ι ι A) :
-    discr A ((P.map (algebraMap A B)).vecMul b) = P.det ^ 2 * discr A b := by
+    discr A (b ᵥ* P.map (algebraMap A B)) = P.det ^ 2 * discr A b := by
   rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ←
     mul_assoc, discr_def, pow_two]
 #align algebra.discr_of_matrix_vec_mul Algebra.discr_of_matrix_vecMul
 
 /-- Relation between `Algebra.discr A ι b` and
-`Algebra.discr A ((P.map (algebraMap A B)).mulVec b)`. -/
+`Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b)`. -/
 theorem discr_of_matrix_mulVec (b : ι → B) (P : Matrix ι ι A) :
-    discr A ((P.map (algebraMap A B)).mulVec b) = P.det ^ 2 * discr A b := by
+    discr A (P.map (algebraMap A B) *ᵥ b) = P.det ^ 2 * discr A b := by
   rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ←
     mul_assoc, discr_def, pow_two]
 #align algebra.discr_of_matrix_mul_vec Algebra.discr_of_matrix_mulVec
@@ -295,7 +295,7 @@ theorem discr_mul_isIntegral_mem_adjoin [IsSeparable K L] [IsIntegrallyClosed R]
   have hinv : IsUnit (traceMatrix K B.basis).det := by
     simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
   have H :
-    (traceMatrix K B.basis).det • (traceMatrix K B.basis).mulVec (B.basis.equivFun z) =
+    (traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
       (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) :=
     by congr; exact traceMatrix_of_basis_mulVec _ _
   have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean
index 102562ae73030..29f271d1bb5a7 100644
--- a/Mathlib/RingTheory/Trace.lean
+++ b/Mathlib/RingTheory/Trace.lean
@@ -478,7 +478,7 @@ theorem traceMatrix_reindex {κ' : Type*} (b : Basis κ A B) (f : κ ≃ κ') :
 variable {A}
 
 theorem traceMatrix_of_matrix_vecMul [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
-    traceMatrix A ((P.map (algebraMap A B)).vecMul b) = Pᵀ * traceMatrix A b * P := by
+    traceMatrix A (b ᵥ* P.map (algebraMap A B)) = Pᵀ * traceMatrix A b * P := by
   ext (α β)
   rw [traceMatrix_apply, vecMul, dotProduct, vecMul, dotProduct, Matrix.mul_apply,
     BilinForm.sum_left,
@@ -499,7 +499,7 @@ theorem traceMatrix_of_matrix_vecMul [Fintype κ] (b : κ → B) (P : Matrix κ
 #align algebra.trace_matrix_of_matrix_vec_mul Algebra.traceMatrix_of_matrix_vecMul
 
 theorem traceMatrix_of_matrix_mulVec [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
-    traceMatrix A ((P.map (algebraMap A B)).mulVec b) = P * traceMatrix A b * Pᵀ := by
+    traceMatrix A (P.map (algebraMap A B) *ᵥ b) = P * traceMatrix A b * Pᵀ := by
   refine' AddEquiv.injective (transposeAddEquiv κ κ A) _
   rw [transposeAddEquiv_apply, transposeAddEquiv_apply, ← vecMul_transpose, ← transpose_map,
     traceMatrix_of_matrix_vecMul, transpose_transpose, transpose_mul, transpose_transpose,
@@ -513,9 +513,9 @@ theorem traceMatrix_of_basis [Fintype κ] [DecidableEq κ] (b : Basis κ A B) :
 #align algebra.trace_matrix_of_basis Algebra.traceMatrix_of_basis
 
 theorem traceMatrix_of_basis_mulVec (b : Basis ι A B) (z : B) :
-    (traceMatrix A b).mulVec (b.equivFun z) = fun i => trace A B (z * b i) := by
+    traceMatrix A b *ᵥ b.equivFun z = fun i => trace A B (z * b i) := by
   ext i
-  rw [← col_apply ((traceMatrix A b).mulVec (b.equivFun z)) i Unit.unit, col_mulVec,
+  rw [← col_apply (traceMatrix A b *ᵥ b.equivFun z) i Unit.unit, col_mulVec,
     Matrix.mul_apply, traceMatrix]
   simp only [col_apply, traceForm_apply]
   conv_lhs =>
diff --git a/Mathlib/Topology/Instances/Matrix.lean b/Mathlib/Topology/Instances/Matrix.lean
index 5769bfe257596..e675856005985 100644
--- a/Mathlib/Topology/Instances/Matrix.lean
+++ b/Mathlib/Topology/Instances/Matrix.lean
@@ -150,14 +150,14 @@ theorem Continuous.matrix_vecMulVec [Mul R] [ContinuousMul R] {A : X → m → R
 @[continuity]
 theorem Continuous.matrix_mulVec [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R]
     [Fintype n] {A : X → Matrix m n R} {B : X → n → R} (hA : Continuous A) (hB : Continuous B) :
-    Continuous fun x => (A x).mulVec (B x) :=
+    Continuous fun x => A x *ᵥ B x :=
   continuous_pi fun i => ((continuous_apply i).comp hA).matrix_dotProduct hB
 #align continuous.matrix_mul_vec Continuous.matrix_mulVec
 
 @[continuity]
 theorem Continuous.matrix_vecMul [NonUnitalNonAssocSemiring R] [ContinuousAdd R] [ContinuousMul R]
     [Fintype m] {A : X → m → R} {B : X → Matrix m n R} (hA : Continuous A) (hB : Continuous B) :
-    Continuous fun x => vecMul (A x) (B x) :=
+    Continuous fun x => A x ᵥ* B x :=
   continuous_pi fun _i => hA.matrix_dotProduct <| continuous_pi fun _j => hB.matrix_elem _ _
 #align continuous.matrix_vec_mul Continuous.matrix_vecMul
 
diff --git a/test/matrix.lean b/test/matrix.lean
index 319e25ea85dd3..29854c7db018b 100644
--- a/test/matrix.lean
+++ b/test/matrix.lean
@@ -93,7 +93,7 @@ example {a a' b b' c c' d d' : α} :
 by simp
 
 example {a b c d x y : α} :
-  mulVec !![a, b; c, d] ![x, y] = ![a * x + b * y, c * x + d * y] :=
+  !![a, b; c, d] *ᵥ ![x, y] = ![a * x + b * y, c * x + d * y] :=
 by simp
 
 /-!