finsuppLeft' — Mathlib

English

When M is also an S-module, the construction finsuppLeft' yields an S-linear equivalence between (ι →₀ M) ⊗ N and ι →₀ (M ⊗ N).

Русский

Пусть M — S-модуль; тогда finsuppLeft' задаёт S-линейное эквивалентное отображение между (ι →₀ M) ⊗ N и ι →₀ (M ⊗ N).

LaTeX

$$$ finsuppLeft' R M N ι S : (ι \\to_0 M) \\otimes_R N \\\\cong_S ι \\to_0 (M \\otimes_R N) $$$

Lean4

/-- When `M` is also an `S`-module, then `TensorProduct.finsuppLeft R M N``
  is an `S`-linear equiv -/
noncomputable def finsuppLeft' : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N
    where
  __ := finsuppLeft R M N ι
  map_smul' := finsuppLeft_smul'

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