finsuppTensorFinsupp'_single_tmul_single

English

For a, b, r1, r2 ∈ the appropriate types, finsuppTensorFinsupp'_single_tmul_single gives Finsupp.single (a,b) (r1 * r2).

Русский

Для a,b, r1, r2 множества типов, finsuppTensorFinsupp'_single_tmul_single возвращает Finsupp.single (a,b) (r1 · r2).

LaTeX

$$$$ \\bigl(\\mathrm{finsuppTensorFinsupp'}\\, R\\, \\iota\\, \\kappa\\bigr)(\\mathrm{Finsupp.single}\\ a\\ r1 \\otimes_R \\mathrm{Finsupp.single}\\ b\\ r2) = \\mathrm{Finsupp.single}\\ (a,b) (r1 \\cdot r2). $$$$

Lean4

@[simp]
theorem finsuppTensorFinsupp'_single_tmul_single (a : ι) (b : κ) (r₁ r₂ : R) :
    finsuppTensorFinsupp' R ι κ (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂) :=
  finsuppTensorFinsuppLid_single_tmul_single R R ι κ a b r₁ r₂

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