Theorems · Definition · linear algebra

LinearMap.uncurryMid

{R : Type uR} →
  {n : ℕ} →
    {M : Fin n.succ → Type v} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : Fin n.succ) → Module R (M i)] →
                [inst_4 : Module R M₂] →
                  (p : Fin (n + 1)) →
                    (M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) → MultilinearMap R M M₂

Given a linear map from M p to the space of multilinear maps in n variables M 0, ..., M n with M p removed, returns a multilinear map in all n + 1 variables.

Defined in

Mathlib.LinearAlgebra.Multilinear.Curry

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule