Theorems · Theorem · linear algebra

finsuppTensorFinsuppLid_apply_apply

∀ (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid N]
  [inst_2 : Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ),
  ((finsuppTensorFinsuppLid R N ι κ) (f ⊗ₜ[R] g)) (a, b) = f a • g b

Defined in

Mathlib.LinearAlgebra.DirectSum.Finsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule