Theorems · Definition · linear algebra

MultilinearMap.piFamily

{ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {M : (i : ι) → κ i → Type uM} →
        {N : ((i : ι) → κ i) → Type uN} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] →
              [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] →
                [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] →
                  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] →
                    ((p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)) →
                      MultilinearMap R (fun i => (j : κ i) → M i j) ((t : (i : ι) → κ i) → N t)

Given a family of indices κ and a multilinear map f p for each way p to select one index from each family, piFamily f maps a family of functions (one for each domain κ i) into a function from each selection of indices (with domain Π i, κ i).

Defined in

Mathlib.LinearAlgebra.Multilinear.Pi

Cited by

9 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModule