Theorems · Theorem · linear algebra

MultilinearMap.freeDFinsuppEquiv_apply

∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {ι' : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : (i : ι) → Fintype (κ i)] [inst_4 : (i : ι) → DecidableEq (κ i)]
  [inst_5 : DecidableEq ι'] [inst_6 : Fintype ι'] (f : Π₀ (x : ((i : ι) → κ i) × ι'), R)
  (x : (i : ι) → Π₀ (x : κ i), R), (MultilinearMap.freeDFinsuppEquiv f) x = ∑ p, f p • fun₀ | p.2 => ∏ i, (x i) (p.1 i)

Defined in

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommSemiringFintypeDecidableEqDecidableEqFintype