Theorems · Definition · linear algebra

vecMulVecBilin

{m : Type u_2} →
  {n : Type u_3} →
    (R : Type u_4) →
      (S : Type u_5) →
        {A : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : Module R A] →
                  [inst_4 : Module S A] →
                    [inst_5 : SMulCommClass S R A] →
                      [SMulCommClass S A A] → [IsScalarTower R A A] → (m → A) →ₗ[R] (n → A) →ₗ[S] Matrix m n A

vecMulVec as a bilinear map. When A is noncommutative, R and S can be instantiated as vecMulVecBilin A Aᵐᵒᵖ.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

1 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiringNonUnitalNonAssocSemiringModuleModuleSMulCommClassSMulCommClassIsScalarTower