Theorems · Definition · linear algebra

mulLinearMap

{l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      (R : Type u_5) →
        {A : Type u_6} →
          [Fintype m] →
            [inst : CommSemiring R] →
              [inst_1 : NonUnitalNonAssocSemiring A] →
                [inst_2 : 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.

Defined in

Mathlib.LinearAlgebra.Matrix.Bilinear

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeCommSemiringNonUnitalNonAssocSemiringModuleSMulCommClassIsScalarTower