finsuppTensorFinsuppLid — Mathlib

English

For i ∈ ι, the symmetric image of Finsupp.single i (m ⊗ n) equals (Finsupp.single i m) ⊗ (Finsupp.single i 1) ⊗ n.

Русский

Для i ∈ ι симметрическое изображение Finsupp.single i (m ⊗ n) равно (Finsupp.single i m) ⊗ (Finsupp.single i 1) ⊗ n.

LaTeX

$$$ (finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m \\otimes n)) = Finsupp.single i.1 m \\otimesₜ Finsupp.single i.2 n $$$

Lean4

/-- A variant of `finsuppTensorFinsupp` where the first module is the ground ring. -/
def finsuppTensorFinsuppLid : (ι →₀ R) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ N :=
  finsuppTensorFinsupp R R R N ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.lid R N)

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