English
The symmetric inverse of finsuppTensorFinsuppRid evaluated at Finsupp.single i (r • m) equals Finsupp.single i.1 r ⊗ Finsupp.single i.2 1, i ∈ ι × κ.
Русский
Обратное к симметрическому отображению finsuppTensorFinsuppRid в точке Finsupp.single i (r • m) равно Finsupp.single i.1 r ⊗ Finsupp.single i.2 1, где i ∈ ι × κ.
LaTeX
$$$$ (\\mathrm{finsuppTensorFinsuppRid}\\, R\\, M\\, \\iota\\, \\kappa)^{-1} (\\mathrm{Finsupp.single}\\ i\\ (r \\cdot m)) = \\mathrm{Finsupp.single}\\ i.1\\ r \\otimes \\mathrm{Finsupp.single}\\ i.2\\ 1. $$$$
Lean4
/-- A variant of `finsuppTensorFinsupp` where both modules are the ground ring. -/
def finsuppTensorFinsupp' : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R :=
finsuppTensorFinsuppLid R R ι κ
