Theorems · Inductive type · linear algebra

MultilinearMap

(R : Type uR) →
  {ι : Type uι} →
    (M₁ : ι → Type v₁) →
      (M₂ : Type v₂) →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] → [(i : ι) → Module R (M₁ i)] → [Module R M₂] → Type (max (max uι v₁) v₂)

Multilinear maps over the ring R, from ∀ i, M₁ i to M₂ where M₁ i and M₂ are modules over R.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

370 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule