Theorems · Theorem · linear algebra

finsuppTensorFinsuppRid_single_tmul_single

∀ (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (a : ι) (b : κ) (m : M) (r : R),
  (finsuppTensorFinsuppRid R M ι κ) ((fun₀ | a => m) ⊗ₜ[R] fun₀ | b => r) = fun₀ | (a, b) => r • m

Defined in

Mathlib.LinearAlgebra.DirectSum.Finsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule