Theorems · Definition · linear algebra

mulLeftLinearMap

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

A version of LinearMap.mulLeft for matrix multiplication.

Defined in

Mathlib.LinearAlgebra.Matrix.Bilinear

Cited by

9 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeSemiringNonUnitalNonAssocSemiringModuleSMulCommClass