Theorems · Definition · linear algebra

LinearMap.BilinMap

(R : Type u_2) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (Nₗ : Type u_8) →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid Nₗ] → [Module R M] → [Module R Nₗ] → Type (max u_8 u_5)

A shorthand for the type of R-bilinear Nₗ-valued maps on M.

Defined in

Mathlib.LinearAlgebra.BilinearMap

Cited by

85 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule