finsuppTensorFinsuppRid_apply_apply

English

The bilinear isomorphism finsuppTensorFinsuppRid satisfies: for f ∈ ι →₀ M and g ∈ κ →₀ R and a ∈ ι, b ∈ κ, (f ⊗ g)(a,b) = g(b) • f(a).

Русский

Билинейное изоморфизмное отображение удовлетворяет: для f ∈ ι →₀ M и g ∈ κ →₀ R и a ∈ ι, b ∈ κ, (f ⊗ g)(a,b) = g(b) • f(a).

LaTeX

$$$$ (\\mathrm{finsuppTensorFinsuppRid}\\, R\\, M\\, \\iota\\, \\kappa)(f \\otimes_R g)(a,b) = g(b) \\cdot f(a). $$$$

Lean4

@[simp]
theorem finsuppTensorFinsuppRid_apply_apply (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) :
    finsuppTensorFinsuppRid R M ι κ (f ⊗ₜ[R] g) (a, b) = g b • f a := by simp [finsuppTensorFinsuppRid]

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