Theorems · Theorem · linear algebra

PiTensorProduct.ofDFinsuppEquiv_tprod_apply

∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : (i : ι) → DecidableEq (κ i)]
  (x : (i : ι) → Π₀ (j : κ i), M i j) (p : (i : ι) → κ i),
  (PiTensorProduct.ofDFinsuppEquiv ((PiTensorProduct.tprod R) x)) p = (PiTensorProduct.tprod R) fun i => (x i) (p i)

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFintypeDecidableEqDecidableEq