English
The map finsuppTensorFinsupp acts on f ⊗ g by sending it to a function that picks out coordinates i, k with f i and g k giving elements in M and N, respectively.
Русский
Отображение finsuppTensorFinsupp действует на f ⊗ g, отправляя его в функцию, которая выбирает координаты i, k с f_i и g_k дающими элементы в M и N соответственно.
LaTeX
$$$ finsuppTensorFinsupp R S M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k $$$
Lean4
@[simp]
theorem finsuppTensorFinsupp_apply (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
finsuppTensorFinsupp R S M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k := by
induction f using Finsupp.induction_linear with
| zero => simp
| add f₁ f₂ hf₁ hf₂ => simp [add_tmul, hf₁, hf₂]
| single i' m =>
induction g using Finsupp.induction_linear with
| zero => simp
| add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
| single k' n =>
classical
simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
split_ifs <;> simp
