Theorems · Definition · linear algebra

LinearMap.compMultilinearMap

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

Composing a multilinear map with a linear map gives again a multilinear map.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

44 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext

Assumes

SemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModule