Documentation

Mathlib.Data.Matrix.Mul

Matrix multiplication #

This file defines vector and matrix multiplication

Main definitions #

Notation #

The locale Matrix gives the following notation:

See Mathlib/Data/Matrix/ConjTranspose.lean for

Implementation notes #

For convenience, Matrix m n α is defined as m → n → α, as this allows elements of the matrix to be accessed with A i j. However, it is not advisable to construct matrices using terms of the form fun i j ↦ _ or even (fun i j ↦ _ : Matrix m n α), as these are not recognized by Lean as having the right type. Instead, Matrix.of should be used.

TODO #

Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.

def dotProduct {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : mα) :
α

dotProduct v w is the sum of the entrywise products v i * w i

Equations
    Instances For
      @[deprecated dotProduct (since := "2024-12-12")]
      def Matrix.dotProduct {m : Type u_2} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] (v w : mα) :
      α

      Alias of dotProduct.


      dotProduct v w is the sum of the entrywise products v i * w i

      Equations
        Instances For

          dotProduct v w is the sum of the entrywise products v i * w i

          Equations
            Instances For
              theorem dotProduct_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : mα) (w : nα) (v : Matrix m n α) :
              (fun (j : n) => u ⬝ᵥ fun (i : m) => v i j) ⬝ᵥ w = u ⬝ᵥ fun (i : m) => v i ⬝ᵥ w
              @[deprecated dotProduct_assoc (since := "2024-12-12")]
              theorem Matrix.dotProduct_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalSemiring α] (u : mα) (w : nα) (v : Matrix m n α) :
              (fun (j : n) => u ⬝ᵥ fun (i : m) => v i j) ⬝ᵥ w = u ⬝ᵥ fun (i : m) => v i ⬝ᵥ w

              Alias of dotProduct_assoc.

              theorem dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommMagma α] (v w : mα) :
              v ⬝ᵥ w = w ⬝ᵥ v
              @[deprecated dotProduct_comm (since := "2024-12-12")]
              theorem Matrix.dotProduct_comm {m : Type u_2} {α : Type v} [Fintype m] [AddCommMonoid α] [CommMagma α] (v w : mα) :
              v ⬝ᵥ w = w ⬝ᵥ v

              Alias of dotProduct_comm.

              @[simp]
              theorem dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v w : PUnit.{u_10 + 1}α) :
              @[deprecated dotProduct_pUnit (since := "2024-12-12")]
              theorem Matrix.dotProduct_pUnit {α : Type v} [AddCommMonoid α] [Mul α] (v w : PUnit.{u_10 + 1}α) :

              Alias of dotProduct_pUnit.

              theorem dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : nα) :
              v ⬝ᵥ 1 = i : n, v i
              @[deprecated dotProduct_one (since := "2024-12-12")]
              theorem Matrix.dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : nα) :
              v ⬝ᵥ 1 = i : n, v i

              Alias of dotProduct_one.

              theorem one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : nα) :
              1 ⬝ᵥ v = i : n, v i
              @[deprecated one_dotProduct (since := "2024-12-12")]
              theorem Matrix.one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [MulOneClass α] [AddCommMonoid α] (v : nα) :
              1 ⬝ᵥ v = i : n, v i

              Alias of one_dotProduct.

              @[simp]
              theorem dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              v ⬝ᵥ 0 = 0
              @[deprecated dotProduct_zero (since := "2024-12-12")]
              theorem Matrix.dotProduct_zero {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              v ⬝ᵥ 0 = 0

              Alias of dotProduct_zero.

              @[simp]
              theorem dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              (v ⬝ᵥ fun (x : m) => 0) = 0
              @[deprecated dotProduct_zero' (since := "2024-12-12")]
              theorem Matrix.dotProduct_zero' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              (v ⬝ᵥ fun (x : m) => 0) = 0

              Alias of dotProduct_zero'.

              @[simp]
              theorem zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              0 ⬝ᵥ v = 0
              @[deprecated zero_dotProduct (since := "2024-12-12")]
              theorem Matrix.zero_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              0 ⬝ᵥ v = 0

              Alias of zero_dotProduct.

              @[simp]
              theorem zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              (fun (x : m) => 0) ⬝ᵥ v = 0
              @[deprecated zero_dotProduct' (since := "2024-12-12")]
              theorem Matrix.zero_dotProduct' {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (v : mα) :
              (fun (x : m) => 0) ⬝ᵥ v = 0

              Alias of zero_dotProduct'.

              @[simp]
              theorem add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : mα) :
              (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
              @[deprecated add_dotProduct (since := "2024-12-12")]
              theorem Matrix.add_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : mα) :
              (u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w

              Alias of add_dotProduct.

              @[simp]
              theorem dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : mα) :
              u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
              @[deprecated dotProduct_add (since := "2024-12-12")]
              theorem Matrix.dotProduct_add {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocSemiring α] (u v w : mα) :
              u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w

              Alias of dotProduct_add.

              @[simp]
              theorem sumElim_dotProduct_sumElim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : mα) (x y : nα) :
              @[deprecated sumElim_dotProduct_sumElim (since := "2024-12-12")]
              theorem Matrix.sum_elim_dotProduct_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : mα) (x y : nα) :

              Alias of sumElim_dotProduct_sumElim.

              @[deprecated sumElim_dotProduct_sumElim (since := "2025-02-21")]
              theorem sum_elim_dotProduct_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u v : mα) (x y : nα) :

              Alias of sumElim_dotProduct_sumElim.

              @[simp]
              theorem comp_equiv_symm_dotProduct {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : mα) (x : nα) (e : m n) :
              u e.symm ⬝ᵥ x = u ⬝ᵥ x e

              Permuting a vector on the left of a dot product can be transferred to the right.

              @[deprecated comp_equiv_symm_dotProduct (since := "2024-12-12")]
              theorem Matrix.comp_equiv_symm_dotProduct {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : mα) (x : nα) (e : m n) :
              u e.symm ⬝ᵥ x = u ⬝ᵥ x e

              Alias of comp_equiv_symm_dotProduct.


              Permuting a vector on the left of a dot product can be transferred to the right.

              @[simp]
              theorem dotProduct_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : mα) (x : nα) (e : n m) :
              u ⬝ᵥ x e.symm = u e ⬝ᵥ x

              Permuting a vector on the right of a dot product can be transferred to the left.

              @[deprecated dotProduct_comp_equiv_symm (since := "2024-12-12")]
              theorem Matrix.dotProduct_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (u : mα) (x : nα) (e : n m) :
              u ⬝ᵥ x e.symm = u e ⬝ᵥ x

              Alias of dotProduct_comp_equiv_symm.


              Permuting a vector on the right of a dot product can be transferred to the left.

              @[simp]
              theorem comp_equiv_dotProduct_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (x y : nα) (e : m n) :
              x e ⬝ᵥ y e = x ⬝ᵥ y

              Permuting vectors on both sides of a dot product is a no-op.

              @[deprecated comp_equiv_dotProduct_comp_equiv (since := "2024-12-12")]
              theorem Matrix.comp_equiv_dotProduct_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] (x y : nα) (e : m n) :
              x e ⬝ᵥ y e = x ⬝ᵥ y

              Alias of comp_equiv_dotProduct_comp_equiv.


              Permuting vectors on both sides of a dot product is a no-op.

              @[simp]
              theorem diagonal_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              Matrix.diagonal v i ⬝ᵥ w = v i * w i
              @[deprecated diagonal_dotProduct (since := "2024-12-12")]
              theorem Matrix.diagonal_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              diagonal v i ⬝ᵥ w = v i * w i

              Alias of diagonal_dotProduct.

              @[simp]
              theorem dotProduct_diagonal {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              v ⬝ᵥ Matrix.diagonal w i = v i * w i
              @[deprecated dotProduct_diagonal (since := "2024-12-12")]
              theorem Matrix.dotProduct_diagonal {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              v ⬝ᵥ diagonal w i = v i * w i

              Alias of dotProduct_diagonal.

              @[simp]
              theorem dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              (v ⬝ᵥ fun (j : m) => Matrix.diagonal w j i) = v i * w i
              @[deprecated dotProduct_diagonal' (since := "2024-12-12")]
              theorem Matrix.dotProduct_diagonal' {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v w : mα) (i : m) :
              (v ⬝ᵥ fun (j : m) => diagonal w j i) = v i * w i

              Alias of dotProduct_diagonal'.

              @[simp]
              theorem single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : mα) (x : α) (i : m) :
              Pi.single i x ⬝ᵥ v = x * v i
              @[deprecated single_dotProduct (since := "2024-12-12")]
              theorem Matrix.single_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : mα) (x : α) (i : m) :
              Pi.single i x ⬝ᵥ v = x * v i

              Alias of single_dotProduct.

              @[simp]
              theorem dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : mα) (x : α) (i : m) :
              v ⬝ᵥ Pi.single i x = v i * x
              @[deprecated dotProduct_single (since := "2024-12-12")]
              theorem Matrix.dotProduct_single {m : Type u_2} {α : Type v} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring α] (v : mα) (x : α) (i : m) :
              v ⬝ᵥ Pi.single i x = v i * x

              Alias of dotProduct_single.

              @[simp]
              theorem one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] :
              1 ⬝ᵥ 1 = (Fintype.card n)
              @[deprecated one_dotProduct_one (since := "2024-12-12")]
              theorem Matrix.one_dotProduct_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] :
              1 ⬝ᵥ 1 = (Fintype.card n)

              Alias of one_dotProduct_one.

              theorem dotProduct_single_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (v : nα) (i : n) :
              v ⬝ᵥ Pi.single i 1 = v i
              @[deprecated dotProduct_single_one (since := "2024-12-12")]
              theorem Matrix.dotProduct_single_one {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (v : nα) (i : n) :
              v ⬝ᵥ Pi.single i 1 = v i

              Alias of dotProduct_single_one.

              theorem single_one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (i : n) (v : nα) :
              Pi.single i 1 ⬝ᵥ v = v i
              @[deprecated single_one_dotProduct (since := "2024-12-12")]
              theorem Matrix.single_one_dotProduct {n : Type u_3} {α : Type v} [Fintype n] [NonAssocSemiring α] [DecidableEq n] (i : n) (v : nα) :
              Pi.single i 1 ⬝ᵥ v = v i

              Alias of single_one_dotProduct.

              @[simp]
              theorem neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              -v ⬝ᵥ w = -(v ⬝ᵥ w)
              @[deprecated neg_dotProduct (since := "2024-12-12")]
              theorem Matrix.neg_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              -v ⬝ᵥ w = -(v ⬝ᵥ w)

              Alias of neg_dotProduct.

              @[simp]
              theorem dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              v ⬝ᵥ -w = -(v ⬝ᵥ w)
              @[deprecated dotProduct_neg (since := "2024-12-12")]
              theorem Matrix.dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              v ⬝ᵥ -w = -(v ⬝ᵥ w)

              Alias of dotProduct_neg.

              theorem neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              -v ⬝ᵥ -w = v ⬝ᵥ w
              @[deprecated neg_dotProduct_neg (since := "2024-12-12")]
              theorem Matrix.neg_dotProduct_neg {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (v w : mα) :
              -v ⬝ᵥ -w = v ⬝ᵥ w

              Alias of neg_dotProduct_neg.

              @[simp]
              theorem sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : mα) :
              (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
              @[deprecated sub_dotProduct (since := "2024-12-12")]
              theorem Matrix.sub_dotProduct {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : mα) :
              (u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w

              Alias of sub_dotProduct.

              @[simp]
              theorem dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : mα) :
              u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
              @[deprecated dotProduct_sub (since := "2024-12-12")]
              theorem Matrix.dotProduct_sub {m : Type u_2} {α : Type v} [Fintype m] [NonUnitalNonAssocRing α] (u v w : mα) :
              u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w

              Alias of dotProduct_sub.

              @[simp]
              theorem smul_dotProduct {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [IsScalarTower R α α] (x : R) (v w : mα) :
              x v ⬝ᵥ w = x (v ⬝ᵥ w)
              @[deprecated smul_dotProduct (since := "2024-12-12")]
              theorem Matrix.smul_dotProduct {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [IsScalarTower R α α] (x : R) (v w : mα) :
              x v ⬝ᵥ w = x (v ⬝ᵥ w)

              Alias of smul_dotProduct.

              @[simp]
              theorem dotProduct_smul {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [SMulCommClass R α α] (x : R) (v w : mα) :
              v ⬝ᵥ x w = x (v ⬝ᵥ w)
              @[deprecated dotProduct_smul (since := "2024-12-12")]
              theorem Matrix.dotProduct_smul {m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [Monoid R] [Mul α] [AddCommMonoid α] [DistribMulAction R α] [SMulCommClass R α α] (x : R) (v w : mα) :
              v ⬝ᵥ x w = x (v ⬝ᵥ w)

              Alias of dotProduct_smul.

              @[defaultInstance 100]
              instance Matrix.instHMulOfFintypeOfMulOfAddCommMonoid {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] :
              HMul (Matrix l m α) (Matrix m n α) (Matrix l n α)

              M * N is the usual product of matrices M and N, i.e. we have that (M * N) i k is the dot product of the i-th row of M by the k-th column of N. This is currently only defined when m is finite.

              Equations
                theorem Matrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} :
                (M * N) i k = j : m, M i j * N j k
                instance Matrix.instMulOfFintypeOfAddCommMonoid {n : Type u_3} {α : Type v} [Fintype n] [Mul α] [AddCommMonoid α] :
                Mul (Matrix n n α)
                Equations
                  theorem Matrix.mul_apply' {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Mul α] [AddCommMonoid α] {M : Matrix l m α} {N : Matrix m n α} {i : l} {k : n} :
                  (M * N) i k = (fun (j : m) => M i j) ⬝ᵥ fun (j : m) => N j k
                  theorem Matrix.two_mul_expl {R : Type u_10} [NonUnitalNonAssocSemiring R] (A B : Matrix (Fin 2) (Fin 2) R) :
                  (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
                  @[simp]
                  theorem Matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (M : Matrix m n α) (N : Matrix n l α) :
                  a M * N = a (M * N)
                  @[simp]
                  theorem Matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [AddCommMonoid α] [Mul α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] (M : Matrix m n α) (a : R) (N : Matrix n l α) :
                  M * a N = a (M * N)
                  @[simp]
                  theorem Matrix.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) :
                  M * 0 = 0
                  @[simp]
                  theorem Matrix.zero_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) :
                  0 * M = 0
                  theorem Matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (L : Matrix m n α) (M N : Matrix n o α) :
                  L * (M + N) = L * M + L * N
                  theorem Matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (L M : Matrix l m α) (N : Matrix m n α) :
                  (L + M) * N = L * N + M * N
                  @[simp]
                  theorem Matrix.diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (d : mα) (M : Matrix m n α) (i : m) (j : n) :
                  (diagonal d * M) i j = d i * M i j
                  @[simp]
                  theorem Matrix.mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d : nα) (M : Matrix m n α) (i : m) (j : n) :
                  (M * diagonal d) i j = M i j * d j
                  @[simp]
                  theorem Matrix.diagonal_mul_diagonal {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ d₂ : nα) :
                  diagonal d₁ * diagonal d₂ = diagonal fun (i : n) => d₁ i * d₂ i
                  theorem Matrix.diagonal_mul_diagonal' {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (d₁ d₂ : nα) :
                  diagonal d₁ * diagonal d₂ = diagonal fun (i : n) => d₁ i * d₂ i
                  theorem Matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) (a : α) :
                  a M = (diagonal fun (x : m) => a) * M
                  theorem Matrix.op_smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
                  MulOpposite.op a M = M * diagonal fun (x : n) => a
                  def Matrix.addMonoidHomMulLeft {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) :
                  Matrix m n α →+ Matrix l n α

                  Left multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

                  Equations
                    Instances For
                      @[simp]
                      theorem Matrix.addMonoidHomMulLeft_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix l m α) (x : Matrix m n α) :
                      def Matrix.addMonoidHomMulRight {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) :
                      Matrix l m α →+ Matrix l n α

                      Right multiplication by a matrix, as an AddMonoidHom from matrices to matrices.

                      Equations
                        Instances For
                          @[simp]
                          theorem Matrix.addMonoidHomMulRight_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (M : Matrix m n α) (x : Matrix l m α) :
                          theorem Matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : βMatrix l m α) (M : Matrix m n α) :
                          (∑ as, f a) * M = as, f a * M
                          theorem Matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [NonUnitalNonAssocSemiring α] [Fintype m] (s : Finset β) (f : βMatrix m n α) (M : Matrix l m α) :
                          M * as, f a = as, M * f a
                          instance Matrix.Semiring.isScalarTower {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] :
                          IsScalarTower R (Matrix n n α) (Matrix n n α)

                          This instance enables use with smul_mul_assoc.

                          instance Matrix.Semiring.smulCommClass {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α] :
                          SMulCommClass R (Matrix n n α) (Matrix n n α)

                          This instance enables use with mul_smul_comm.

                          @[simp]
                          theorem Matrix.one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (M : Matrix m n α) :
                          1 * M = M
                          @[simp]
                          theorem Matrix.mul_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) :
                          M * 1 = M
                          instance Matrix.nonAssocSemiring {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] [DecidableEq n] :
                          Equations
                            @[simp]
                            theorem Matrix.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [NonAssocSemiring α] [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} :
                            (L * M).map f = L.map f * M.map f
                            theorem Matrix.smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) :
                            a 1 = diagonal fun (x : m) => a
                            theorem Matrix.op_smul_one_eq_diagonal {m : Type u_2} {α : Type v} [NonAssocSemiring α] [DecidableEq m] (a : α) :
                            MulOpposite.op a 1 = diagonal fun (x : m) => a
                            theorem Matrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype m] [Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α) :
                            L * M * N = L * (M * N)
                            instance Matrix.nonUnitalSemiring {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] :
                            Equations
                              instance Matrix.semiring {n : Type u_3} {α : Type v} [Semiring α] [Fintype n] [DecidableEq n] :
                              Semiring (Matrix n n α)
                              Equations
                                @[simp]
                                theorem Matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) :
                                -M * N = -(M * N)
                                @[simp]
                                theorem Matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) :
                                M * -N = -(M * N)
                                theorem Matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M M' : Matrix m n α) (N : Matrix n o α) :
                                (M - M') * N = M * N - M' * N
                                theorem Matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (M : Matrix m n α) (N N' : Matrix n o α) :
                                M * (N - N') = M * N - M * N'
                                instance Matrix.instNonUnitalRing {n : Type u_3} {α : Type v} [Fintype n] [NonUnitalRing α] :
                                Equations
                                  instance Matrix.instNonAssocRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [NonAssocRing α] :
                                  Equations
                                    instance Matrix.instRing {n : Type u_3} {α : Type v} [Fintype n] [DecidableEq n] [Ring α] :
                                    Ring (Matrix n n α)
                                    Equations
                                      @[simp]
                                      theorem Matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Semiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) :
                                      (of fun (i : m) (j : n) => a * M i j) * N = a (M * N)
                                      theorem Matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
                                      a M = M * diagonal fun (x : n) => a
                                      @[simp]
                                      theorem Matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [CommSemiring α] [Fintype n] (M : Matrix m n α) (N : Matrix n o α) (a : α) :
                                      (M * of fun (i : n) (j : o) => a * N i j) = a (M * N)
                                      def Matrix.vecMulVec {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : mα) (v : nα) :
                                      Matrix m n α

                                      For two vectors w and v, vecMulVec w v i j is defined to be w i * v j. Put another way, vecMulVec w v is exactly col w * row v.

                                      Equations
                                        Instances For
                                          theorem Matrix.vecMulVec_apply {m : Type u_2} {n : Type u_3} {α : Type v} [Mul α] (w : mα) (v : nα) (i : m) (j : n) :
                                          vecMulVec w v i j = w i * v j
                                          def Matrix.mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (M : Matrix m n α) (v : nα) :
                                          mα

                                          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 dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

                                          Equations
                                            Instances For

                                              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 dotProduct, so that A *ᵥ v ⬝ᵥ B *ᵥ w is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w).

                                              Equations
                                                Instances For
                                                  def Matrix.vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : mα) (M : Matrix m n α) :
                                                  nα

                                                  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 dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

                                                  Equations
                                                    Instances For

                                                      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 dotProduct, so that v ᵥ* A ⬝ᵥ w ᵥ* B is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B).

                                                      Equations
                                                        Instances For
                                                          def Matrix.mulVec.addMonoidHomLeft {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : nα) :
                                                          Matrix m n α →+ mα

                                                          Left multiplication by a matrix, as an AddMonoidHom from vectors to vectors.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Matrix.mulVec.addMonoidHomLeft_apply {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : nα) (M : Matrix m n α) (a✝ : m) :
                                                              (addMonoidHomLeft v) M a✝ = M.mulVec v a✝
                                                              theorem Matrix.mul_apply_eq_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) :
                                                              (A * B) i = vecMul (A i) B

                                                              The ith row of the multiplication is the same as the vecMul with the ith row of A.

                                                              theorem Matrix.vecMul_eq_sum {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : mα) (M : Matrix m n α) :
                                                              vecMul v M = i : m, v i M i
                                                              theorem Matrix.mulVec_eq_sum {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : nα) (M : Matrix m n α) :
                                                              M.mulVec v = i : n, MulOpposite.op (v i) M.transpose i
                                                              theorem Matrix.mulVec_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v w : mα) (x : m) :
                                                              (diagonal v).mulVec w x = v x * w x
                                                              theorem Matrix.vecMul_diagonal {m : Type u_2} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] [DecidableEq m] (v w : mα) (x : m) :
                                                              vecMul v (diagonal w) x = v x * w x
                                                              theorem Matrix.dotProduct_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : mR) (A : Matrix m n R) (w : nR) :

                                                              Associate the dot product of mulVec to the left.

                                                              @[simp]
                                                              theorem Matrix.mulVec_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) :
                                                              A.mulVec 0 = 0
                                                              @[simp]
                                                              theorem Matrix.zero_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) :
                                                              vecMul 0 A = 0
                                                              @[simp]
                                                              theorem Matrix.zero_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (v : nα) :
                                                              mulVec 0 v = 0
                                                              @[simp]
                                                              theorem Matrix.vecMul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (v : mα) :
                                                              vecMul v 0 = 0
                                                              theorem Matrix.smul_mulVec_assoc {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] [Monoid R] [DistribMulAction R α] [IsScalarTower R α α] (a : R) (A : Matrix m n α) (b : nα) :
                                                              (a A).mulVec b = a A.mulVec b
                                                              theorem Matrix.mulVec_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A : Matrix m n α) (x y : nα) :
                                                              A.mulVec (x + y) = A.mulVec x + A.mulVec y
                                                              theorem Matrix.add_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype n] (A B : Matrix m n α) (x : nα) :
                                                              (A + B).mulVec x = A.mulVec x + B.mulVec x
                                                              theorem Matrix.vecMul_add {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A B : Matrix m n α) (x : mα) :
                                                              vecMul x (A + B) = vecMul x A + vecMul x B
                                                              theorem Matrix.add_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocSemiring α] [Fintype m] (A : Matrix m n α) (x y : mα) :
                                                              vecMul (x + y) A = vecMul x A + vecMul y A
                                                              theorem Matrix.vecMul_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [IsScalarTower R S S] (M : Matrix n m S) (b : R) (v : nS) :
                                                              vecMul (b v) M = b vecMul v M
                                                              theorem Matrix.mulVec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonUnitalNonAssocSemiring S] [DistribSMul R S] [SMulCommClass R S S] (M : Matrix m n S) (b : R) (v : nS) :
                                                              M.mulVec (b v) = b M.mulVec v
                                                              @[simp]
                                                              theorem Matrix.mulVec_single {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (j : n) (x : R) :
                                                              @[simp]
                                                              theorem Matrix.single_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype m] [DecidableEq m] [NonUnitalNonAssocSemiring R] (M : Matrix m n R) (i : m) (x : R) :
                                                              vecMul (Pi.single i x) M = x M.row i
                                                              theorem Matrix.mulVec_single_one {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonAssocSemiring R] (M : Matrix m n R) (j : n) :
                                                              M.mulVec (Pi.single j 1) = M.col j
                                                              theorem Matrix.single_one_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} [Fintype m] [DecidableEq m] [NonAssocSemiring R] (i : m) (M : Matrix m n R) :
                                                              vecMul (Pi.single i 1) M = M.row i
                                                              theorem Matrix.diagonal_mulVec_single {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : nR) (j : n) (x : R) :
                                                              (diagonal v).mulVec (Pi.single j x) = Pi.single j (v j * x)
                                                              theorem Matrix.single_vecMul_diagonal {n : Type u_3} {R : Type u_7} [Fintype n] [DecidableEq n] [NonUnitalNonAssocSemiring R] (v : nR) (j : n) (x : R) :
                                                              vecMul (Pi.single j x) (diagonal v) = Pi.single j (x * v j)
                                                              @[simp]
                                                              theorem Matrix.vecMul_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype m] (v : mα) (M : Matrix m n α) (N : Matrix n o α) :
                                                              vecMul (vecMul v M) N = vecMul v (M * N)
                                                              @[simp]
                                                              theorem Matrix.mulVec_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalSemiring α] [Fintype n] [Fintype o] (v : oα) (M : Matrix m n α) (N : Matrix n o α) :
                                                              M.mulVec (N.mulVec v) = (M * N).mulVec v
                                                              theorem Matrix.mul_mul_apply {n : Type u_3} {α : Type v} [NonUnitalSemiring α] [Fintype n] (A B C : Matrix n n α) (i j : n) :
                                                              (A * B * C) i j = A i ⬝ᵥ B.mulVec (C.transpose j)
                                                              theorem Matrix.mulVec_one {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype n] (A : Matrix m n α) :
                                                              A.mulVec 1 = j : n, A.transpose j
                                                              theorem Matrix.one_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) :
                                                              vecMul 1 A = i : m, A i
                                                              @[deprecated Matrix.one_vecMul (since := "2025-01-26")]
                                                              theorem Matrix.vec_one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [Fintype m] (A : Matrix m n α) :
                                                              vecMul 1 A = i : m, A i

                                                              Alias of Matrix.one_vecMul.

                                                              theorem Matrix.ext_of_mulVec_single {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [DecidableEq n] [Fintype n] {M N : Matrix m n α} (h : ∀ (i : n), M.mulVec (Pi.single i 1) = N.mulVec (Pi.single i 1)) :
                                                              M = N
                                                              theorem Matrix.ext_of_single_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonAssocSemiring α] [DecidableEq m] [Fintype m] {M N : Matrix m n α} (h : ∀ (i : m), vecMul (Pi.single i 1) M = vecMul (Pi.single i 1) N) :
                                                              M = N
                                                              @[simp]
                                                              theorem Matrix.one_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : mα) :
                                                              mulVec 1 v = v
                                                              @[simp]
                                                              theorem Matrix.vecMul_one {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (v : mα) :
                                                              vecMul v 1 = v
                                                              @[simp]
                                                              theorem Matrix.diagonal_const_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : mα) :
                                                              (diagonal fun (x_1 : m) => x).mulVec v = x v
                                                              @[simp]
                                                              theorem Matrix.vecMul_diagonal_const {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : α) (v : mα) :
                                                              vecMul v (diagonal fun (x_1 : m) => x) = MulOpposite.op x v
                                                              @[simp]
                                                              theorem Matrix.natCast_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ) (v : mα) :
                                                              (↑x).mulVec v = x v
                                                              @[simp]
                                                              theorem Matrix.vecMul_natCast {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ) (v : mα) :
                                                              vecMul v x = MulOpposite.op x v
                                                              @[simp]
                                                              theorem Matrix.ofNat_mulVec {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ) [x.AtLeastTwo] (v : mα) :
                                                              @[simp]
                                                              theorem Matrix.vecMul_ofNat {m : Type u_2} {α : Type v} [NonAssocSemiring α] [Fintype m] [DecidableEq m] (x : ) [x.AtLeastTwo] (v : mα) :
                                                              theorem Matrix.neg_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : mα) (A : Matrix m n α) :
                                                              vecMul (-v) A = -vecMul v A
                                                              theorem Matrix.vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : mα) (A : Matrix m n α) :
                                                              vecMul v (-A) = -vecMul v A
                                                              theorem Matrix.neg_vecMul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (v : mα) (A : Matrix m n α) :
                                                              vecMul (-v) (-A) = vecMul v A
                                                              theorem Matrix.neg_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : nα) (A : Matrix m n α) :
                                                              (-A).mulVec v = -A.mulVec v
                                                              theorem Matrix.mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : nα) (A : Matrix m n α) :
                                                              A.mulVec (-v) = -A.mulVec v
                                                              theorem Matrix.neg_mulVec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (v : nα) (A : Matrix m n α) :
                                                              (-A).mulVec (-v) = A.mulVec v
                                                              theorem Matrix.mulVec_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A : Matrix m n α) (x y : nα) :
                                                              A.mulVec (x - y) = A.mulVec x - A.mulVec y
                                                              theorem Matrix.sub_mulVec {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype n] (A B : Matrix m n α) (x : nα) :
                                                              (A - B).mulVec x = A.mulVec x - B.mulVec x
                                                              theorem Matrix.vecMul_sub {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A B : Matrix m n α) (x : mα) :
                                                              vecMul x (A - B) = vecMul x A - vecMul x B
                                                              theorem Matrix.sub_vecMul {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalNonAssocRing α] [Fintype m] (A : Matrix m n α) (x y : mα) :
                                                              vecMul (x - y) A = vecMul x A - vecMul y A
                                                              theorem Matrix.mulVec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] (A : Matrix m n α) (x : mα) :
                                                              theorem Matrix.vecMul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] (A : Matrix m n α) (x : nα) :
                                                              theorem Matrix.mulVec_vecMul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype n] [Fintype o] (A : Matrix m n α) (B : Matrix o n α) (x : oα) :
                                                              A.mulVec (vecMul x B) = (A * B.transpose).mulVec x
                                                              theorem Matrix.vecMul_mulVec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [NonUnitalCommSemiring α] [Fintype m] [Fintype n] (A : Matrix m n α) (B : Matrix m o α) (x : nα) :
                                                              vecMul (A.mulVec x) B = vecMul x (A.transpose * B)
                                                              theorem Matrix.mulVec_injective_of_isUnit {m : Type u_2} {R : Type u_7} [Semiring R] [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) :
                                                              theorem Matrix.vecMul_injective_of_isUnit {m : Type u_2} {R : Type u_7} [Semiring R] [Fintype m] [DecidableEq m] {A : Matrix m m R} (ha : IsUnit A) :
                                                              Function.Injective fun (v : mR) => vecMul v A
                                                              theorem Matrix.mulVec_smul_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [CommSemiring α] [Fintype n] (A : Matrix m n α) (b : nα) (a : α) :
                                                              A.mulVec (a b) = a A.mulVec b
                                                              @[simp]
                                                              theorem Matrix.intCast_mulVec {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ) (v : mα) :
                                                              (↑x).mulVec v = x v
                                                              @[simp]
                                                              theorem Matrix.vecMul_intCast {m : Type u_2} {α : Type v} [NonAssocRing α] [Fintype m] [DecidableEq m] (x : ) (v : mα) :
                                                              vecMul v x = MulOpposite.op x v
                                                              @[simp]
                                                              theorem Matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [AddCommMonoid α] [CommMagma α] [Fintype n] (M : Matrix m n α) (N : Matrix n l α) :
                                                              theorem Matrix.submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : lm) (e₂ : on) (e₃ : qp) (he₂ : Function.Bijective e₂) :
                                                              (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃

                                                              simp lemmas for Matrix.submatrixs interaction with Matrix.diagonal, 1, and Matrix.mul for when the mappings are bundled.

                                                              @[simp]
                                                              theorem Matrix.submatrix_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [AddCommMonoid α] [Mul α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α) (e₁ : lm) (e₂ : o n) (e₃ : qp) :
                                                              M.submatrix e₁ e₂ * N.submatrix (⇑e₂) e₃ = (M * N).submatrix e₁ e₃
                                                              theorem Matrix.submatrix_mulVec_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : oα) (e₁ : lm) (e₂ : o n) :
                                                              (M.submatrix e₁ e₂).mulVec v = M.mulVec (v e₂.symm) e₁
                                                              @[simp]
                                                              theorem Matrix.submatrix_id_mul_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : lm) (e₂ : n o) :
                                                              M.submatrix e₁ id * N.submatrix (⇑e₂) id = M.submatrix e₁ e₂.symm * N
                                                              @[simp]
                                                              theorem Matrix.submatrix_id_mul_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Fintype o] [Mul α] [AddCommMonoid α] {p : Type u_10} (M : Matrix m n α) (N : Matrix o p α) (e₁ : lp) (e₂ : o n) :
                                                              M.submatrix id e₂ * N.submatrix id e₁ = M * N.submatrix (⇑e₂.symm) e₁
                                                              theorem Matrix.submatrix_vecMul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : lα) (e₁ : l m) (e₂ : on) :
                                                              vecMul v (M.submatrix (⇑e₁) e₂) = vecMul (v e₁.symm) M e₂
                                                              theorem Matrix.mul_submatrix_one {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype n] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : n o) (e₂ : lo) (M : Matrix m n α) :
                                                              M * submatrix 1 (⇑e₁) e₂ = M.submatrix id (e₁.symm e₂)
                                                              theorem Matrix.one_submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [Fintype m] [Finite o] [NonAssocSemiring α] [DecidableEq o] (e₁ : lo) (e₂ : m o) (M : Matrix m n α) :
                                                              submatrix 1 e₁ e₂ * M = M.submatrix (e₂.symm e₁) id
                                                              theorem Matrix.submatrix_mul_transpose_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α] (e : m n) (M : Matrix m n α) :
                                                              theorem RingHom.map_matrix_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [Fintype n] [NonAssocSemiring α] [NonAssocSemiring β] (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) :
                                                              f ((M * N) i j) = (M.map f * N.map f) i j
                                                              theorem RingHom.map_dotProduct {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (v w : nR) :
                                                              f (v ⬝ᵥ w) = f v ⬝ᵥ f w
                                                              theorem RingHom.map_vecMul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : nR) (i : m) :
                                                              f (Matrix.vecMul v M i) = Matrix.vecMul (f v) (M.map f) i
                                                              theorem RingHom.map_mulVec {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : nR) (i : m) :
                                                              f (M.mulVec v i) = (M.map f).mulVec (f v) i