Theorems · Definition · linear algebra

dotProductBilin

{m : Type u_2} →
  (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] → [Fintype m] → (m → A) →ₗ[R] (m → A) →ₗ[S] A

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

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringSemiringNonUnitalNonAssocSemiringModuleModuleSMulCommClassSMulCommClassIsScalarTowerFintype