English
There is a canonical linear map from Dual M ⊗ Dual N to Dual (M ⊗ N) sending f ⊗ g to the functional (m ⊗ n) ↦ f(m) g(n).
Русский
Существует каноническое линейное отображение from Dual M ⊗ Dual N в Dual (M ⊗ N), отправляющее f ⊗ g в функционал (m ⊗ n) ↦ f(m) g(n).
LaTeX
$$$$ dualDistrib: Dual_R M \\otimes_R Dual_R N \\to Dual_R (M \\otimes_R N),\\quad (f \\otimes g)(m \\otimes n) = f(m) \\cdot g(n). $$$$
Lean4
/-- The canonical linear map from `Dual M ⊗ Dual N` to `Dual (M ⊗ N)`,
sending `f ⊗ g` to the composition of `TensorProduct.map f g` with
the natural isomorphism `R ⊗ R ≃ R`.
-/
def dualDistrib : Dual R M ⊗[R] Dual R N →ₗ[R] Dual R (M ⊗[R] N) :=
compRight _ (TensorProduct.lid R R) ∘ₗ homTensorHomMap R M N R R
