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)
:
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' := ⋯ }
Instances For
@[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]
:
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)
:
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' := ⋯ }
Instances For
@[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]
:
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]
:
A version of LinearMap.mul for matrix multiplication.
Equations
- mulLinearMap R = { toFun := mulLeftLinearMap n R, map_add' := ⋯, map_smul' := ⋯ }
Instances For
@[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]
[DecidableEq 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]
[DecidableEq 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.