Theorems · Theorem · linear algebra

MultilinearMap.fromDirectSumEquiv_apply

∀ {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']
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] [inst_7 : (i : ι) → DecidableEq (κ i)]
  [inst_8 : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)]
  (f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) M')
  (x : DirectSum ι fun i => DirectSum (κ i) fun j => M i j),
  (MultilinearMap.fromDirectSumEquiv f) ⇑x =
    ∑ p ∈ Fintype.piFinset fun i => DFinsupp.support (x i), (f p) fun i => (x i) (p i)

Prefer using fromDirectSumEquiv_lof where possible.

Defined in

Mathlib.LinearAlgebra.Multilinear.DirectSum

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleDecidableEqFintypeDecidableEqDecidable