Theorems · Definition · linear algebra

MultilinearMap.fromDirectSumEquiv

{R : Type u_1} →
  {ι : Type u_2} →
    {M' : Type u_3} →
      {κ : ι → Type u_4} →
        {M : (i : ι) → κ i → Type u_5} →
          [inst : CommSemiring R] →
            [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] →
              [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] →
                [inst_3 : AddCommMonoid M'] →
                  [inst_4 : Module R M'] →
                    [DecidableEq ι] →
                      [Finite ι] →
                        ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M') ≃ₗ[R]
                          MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M'

The linear equivalence between families indexed by p : Π i : ι, κ i of multilinear maps on the fun i ↦ M i (p i) and the space of multilinear map on fun i ↦ ⨁ j : κ i, M i j.

Defined in

Mathlib.LinearAlgebra.Multilinear.DirectSum

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEqFinite