finsuppTensorFinsuppLid_single_tmul_single

English

For f = Finsupp.single a r and g = Finsupp.single b n, the isomorphism finsuppTensorFinsuppLid sends f ⊗ g to Finsupp.single (a,b) (r • n).

Русский

Для f = Finsupp.single a r и g = Finsupp.single b n отображение FinsuppTensorFinsuppLid отправляет f ⊗ g в Finsupp.single (a,b) (r • n).

LaTeX

$$$$ \\bigl(\\mathrm{finsuppTensorFinsuppLid}\\, R\\, N\\, \\iota\\, \\kappa\\bigr)\\bigl( \\mathrm{Finsupp.single}\\ a\\ r \\otimes_R \\mathrm{Finsupp.single}\\ b\\ n \\bigr) = \\mathrm{Finsupp.single}\\ (a, b)\\ (r \\cdot n). $$$$

Lean4

@[simp]
theorem finsuppTensorFinsuppLid_single_tmul_single (a : ι) (b : κ) (r : R) (n : N) :
    finsuppTensorFinsuppLid R N ι κ (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n) := by
  simp [finsuppTensorFinsuppLid]

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