Bundled versions of multiplication for matrices

This file provides versions of LinearMap.mulLeft and LinearMap.mulRight which work for the heterogeneous multiplication of matrices.

def mulLeftLinearMap {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] (X : Matrix l m A) : Matrix m n A →ₗ[R] Matrix l n A

A version of LinearMap.mulLeft for matrix multiplication.

Equations

• mulLeftLinearMap n R X = { toFun := fun (x : Matrix m n A) => X * x, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem mulLeftLinearMap_apply {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] (X : Matrix l m A) (x✝ : Matrix m n A) : (mulLeftLinearMap n R X) x✝ = X * x✝

theorem mulLeftLinearMap_eq_mulLeft {m : Type u_2} (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] : mulLeftLinearMap m R = LinearMap.mulLeft R

On square matrices, Matrix.mulLeftLinearMap and LinearMap.mulLeft coincide.

@[simp]

theorem mulLeftLinearMap_zero_eq_zero {l : Type u_1} {m : Type u_2} (n : Type u_3) (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] : mulLeftLinearMap n R 0 = 0

A version of LinearMap.mulLeft_zero_eq_zero for matrix multiplication.

def mulRightLinearMap (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (Y : Matrix m n A) : Matrix l m A →ₗ[R] Matrix l n A

A version of LinearMap.mulRight for matrix multiplication.

Equations

• mulRightLinearMap l R Y = { toFun := fun (x : Matrix l m A) => x * Y, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem mulRightLinearMap_apply (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] (Y : Matrix m n A) (x✝ : Matrix l m A) : (mulRightLinearMap l R Y) x✝ = x✝ * Y

theorem mulRightLinearMap_eq_mulRight {m : Type u_2} (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] : mulRightLinearMap m R = LinearMap.mulRight R

On square matrices, Matrix.mulRightLinearMap and LinearMap.mulRight coincide.

@[simp]

theorem mulRightLinearMap_zero_eq_zero (l : Type u_1) {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [Fintype m] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] : mulRightLinearMap l R 0 = 0

A version of LinearMap.mulLeft_zero_eq_zero for matrix multiplication.

def mulLinearMap {l : Type u_1} {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [Fintype m] [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : Matrix l m A →ₗ[R] Matrix m n A →ₗ[R] Matrix l n A

A version of LinearMap.mul for matrix multiplication.

Equations

• mulLinearMap R = { toFun := mulLeftLinearMap n R, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem mulLinearMap_apply_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} (R : Type u_5) {A : Type u_6} [Fintype m] [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (X : Matrix l m A) (x✝ : Matrix m n A) : ((mulLinearMap R) X) x✝ = X * x✝

theorem mulLinearMap_eq_mul {m : Type u_2} (R : Type u_5) {A : Type u_6} [Fintype m] [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] : mulLinearMap R = LinearMap.mul R (Matrix m m A)

On square matrices, Matrix.mulLinearMap and LinearMap.mul coincide.

@[simp]

theorem mulLeftLinearMap_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [Fintype m] [Fintype n] [Semiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] (a : Matrix l m A) (b : Matrix m n A) : mulLeftLinearMap o R (a * b) = mulLeftLinearMap o R a ∘ₗ mulLeftLinearMap o R b

A version of LinearMap.mulLeft_mul for matrix multiplication.

@[simp]

theorem mulRightLinearMap_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [Fintype m] [Fintype n] [Semiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] (a : Matrix m n A) (b : Matrix n o A) : mulRightLinearMap l R (a * b) = mulRightLinearMap l R b ∘ₗ mulRightLinearMap l R a

A version of LinearMap.mulRight_mul for matrix multiplication.

theorem commute_mulLeftLinearMap_mulRightLinearMap {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [Fintype m] [Fintype n] [CommSemiring R] [NonUnitalSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] (a : Matrix l m A) (b : Matrix n o A) : mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b = mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a

A version of LinearMap.commute_mulLeft_right for matrix multiplication.

@[simp]

theorem mulLeftLinearMap_one {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [Fintype m] [DecidableEq m] [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] : mulLeftLinearMap n R 1 = LinearMap.id

A version of LinearMap.mulLeft_one for matrix multiplication.

@[simp]

theorem mulLeftLinearMap_eq_zero_iff {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [Fintype m] [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] [Nonempty n] (a : Matrix l m A) : mulLeftLinearMap n R a = 0 ↔ a = 0

A version of LinearMap.mulLeft_eq_zero_iff for matrix multiplication.

@[simp]

theorem pow_mulLeftLinearMap {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [Fintype m] [DecidableEq m] [Semiring R] [Semiring A] [Module R A] [SMulCommClass R A A] (a : Matrix m m A) (k : ℕ) : mulLeftLinearMap n R a ^ k = mulLeftLinearMap n R (a ^ k)

A version of LinearMap.pow_mulLeft for matrix multiplication.

@[simp]

theorem mulRightLinearMap_one {l : Type u_1} {m : Type u_2} {R : Type u_5} {A : Type u_6} [Fintype m] [DecidableEq m] [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] : mulRightLinearMap l R 1 = LinearMap.id

A version of LinearMap.mulRight_one for matrix multiplication.

@[simp]

theorem mulRightLinearMap_eq_zero_iff {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_5} {A : Type u_6} [Fintype m] [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] (a : Matrix m n A) [Nonempty l] : mulRightLinearMap l R a = 0 ↔ a = 0

A version of LinearMap.mulRight_eq_zero_iff for matrix multiplication.

@[simp]

theorem pow_mulRightLinearMap {l : Type u_1} {m : Type u_2} {R : Type u_5} {A : Type u_6} [Fintype m] [DecidableEq m] [Semiring R] [Semiring A] [Module R A] [IsScalarTower R A A] (a : Matrix m m A) (k : ℕ) : mulRightLinearMap l R a ^ k = mulRightLinearMap l R (a ^ k)

A version of LinearMap.pow_mulRight for matrix multiplication.