finsuppTensorFinsuppRid_single_tmul_single

English

If f = Finsupp.single a m and g = Finsupp.single b r, then (finsuppTensorFinsuppRid R M ι κ)(f ⊗ g) = Finsupp.single (a,b) (r • m).

Русский

Если f = Finsupp.single a m и g = Finsupp.single b r, то (finsuppTensorFinsuppRid R M ι κ)(f ⊗ g) = Finsupp.single (a,b) (r • m).

LaTeX

$$$$ \\bigl(\\mathrm{finsuppTensorFinsuppRid}\\, R\\, M\\, \\iota\\, \\kappa\\bigr)\\bigl( \\mathrm{Finsupp.single}\\ a\\ m \\otimes_R \\mathrm{Finsupp.single}\\ b\\ r \\bigr) = \\mathrm{Finsupp.single}\\ (a,b)\\ (r \\cdot m). $$$$

Lean4

@[simp]
theorem finsuppTensorFinsuppRid_single_tmul_single (a : ι) (b : κ) (m : M) (r : R) :
    finsuppTensorFinsuppRid R M ι κ (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m) := by
  simp [finsuppTensorFinsuppRid]

Похожие утверждения