Theorems · Definition · linear algebra

MultilinearMap.toLinearMap

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

If f is a multilinear map, then f.toLinearMap m i is the linear map obtained by fixing all coordinates but i equal to those of m, and varying the i-th coordinate.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

5 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleDecidableEq