finsuppTensorFinsupp_single — Mathlib

English

The isomorphism finsuppTensorFinsupp sends a simple tensor of singletons to a singleton indexed by the pair (i, k) with the tensor product m ⊗ n.

Русский

Изоморфизм finsuppTensorFinsupp отправляет простой тензор из одиночек в одиночку с индексом пары (i, k) и тензорным произведением m ⊗ n.

LaTeX

$$$ finsuppTensorFinsupp R S M N ι κ (Finsupp.single i m) ⊗ₜ Finsupp.single k n = Finsupp.single (i, k) (m ⊗ₜ n) $$$

Lean4

@[simp]
theorem finsuppTensorFinsupp_single (i : ι) (m : M) (k : κ) (n : N) :
    finsuppTensorFinsupp R S M N ι κ (Finsupp.single i m ⊗ₜ Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ n) := by
  simp [finsuppTensorFinsupp]

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