Theorems · Definition · linear algebra

MultilinearMap.currySum

{R : Type uR} →
  {ι : Type uι} →
    {ι' : Type uι'} →
      {M₂ : Type v₂} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : Module R M₂] →
              {N : ι ⊕ ι' → Type u_1} →
                [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)] →
                  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] →
                    MultilinearMap R N M₂ →
                      MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)

Given a family of modules N : (ι ⊕ ι') → Type*, a multilinear map on (fun _ : ι ⊕ ι' => M') induces a multilinear map on (fun (i : ι) ↦ N (.inl i)) taking values in the space of linear maps on (fun (i : ι') ↦ N (.inr i)).

Defined in

Mathlib.LinearAlgebra.Multilinear.Curry

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule