Theorems · Theorem · linear algebra

PiTensorProduct.dualDistrib_apply

∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (f : (i : ι) → Module.Dual R (M i)) (m : (i : ι) → M i),
  (PiTensorProduct.dualDistrib ((PiTensorProduct.tprod R) fun i => f i)) (⨂ₜ[R] (i : ι), m i) = ∏ i, (f i) (m i)

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Dual

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFintype