English
Let f ∈ ι →₀ R and g ∈ κ →₀ N. Under the canonical isomorphism between the tensor product (ι →₀ R) ⊗ (κ →₀ N) and ι × κ →₀ N, the value at (a, b) of (f ⊗ g) is f(a) acting on g(b). In particular, the image at (a,b) is f(a) • g(b).
Русский
Пусть f ∈ ι →₀ R и g ∈ κ →₀ N. При переходе через канонический изоморфизм между тензорным произведением и Finsupp-модулем значение в точке (a, b) для (f ⊗ g) равно f(a) • g(b). В частности, на позиции (a,b) получается f(a) • g(b).
LaTeX
$$$$ \\bigl(\\mathrm{finsuppTensorFinsuppLid}\, R\\, N\\, \\iota\\, \\kappa\\bigr)\\bigl(f \\otimes_R g\\bigr)(a, b) = f(a) \\cdot g(b). $$$$
Lean4
@[simp]
theorem finsuppTensorFinsuppLid_apply_apply (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) :
finsuppTensorFinsuppLid R N ι κ (f ⊗ₜ[R] g) (a, b) = f a • g b := by simp [finsuppTensorFinsuppLid]
