Documentation

Mathlib.Data.Matrix.Bilinear

Bundled versions of multiplication for matrices #

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

source
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
    Instances For
      source
      @[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✝
      source
      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.

      source
      @[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.

      source
      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
        Instances For
          source
          @[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
          source
          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.

          source
          @[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.

          source
          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
            Instances For
              source
              @[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✝
              source
              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.

              source
              @[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.

              source
              @[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.

              source
              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.

              source
              @[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.

              source
              @[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.

              source
              @[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.

              source
              @[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.

              source
              @[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.

              source
              @[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.