Theorems · Definition · linear algebra

MultilinearMap.fromDFinsuppEquiv

{ι : Type uι} →
  (κ : ι → Type uκ) →
    (R : Type uR) →
      {M : (i : ι) → κ i → Type uM} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
                [inst_2 : (i : ι) → (k : κ i) → Module R (M i k)] →
                  {N : Type u_1} →
                    [inst_3 : AddCommMonoid N] →
                      [inst_4 : Module R N] →
                        [(i : ι) → DecidableEq (κ i)] →
                          ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) N) ≃ₗ[R]
                            MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N

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.DFinsupp

Cited by

8 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommSemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEq