English
If M is a finite free module over a commutative semiring R, then the natural pairing (M → P) ⊗_R Q is canonically isomorphic to M → (P ⊗_R Q).
Русский
Если модуль M над R является конечным свободным, то естественное сопряжение \u2060 (M → P) ⊗_R Q \u2060 изоморфно как M → (P ⊗_R Q).
LaTeX
$$$(M \to_R P) \otimes_R Q \;\cong_R\; M \to_R (P \otimes_R Q)$$$
Lean4
/-- When `M` is a finite free module, the map `rTensorHomToHomRTensor` is an equivalence. Note
that `rTensorHomEquivHomRTensor` is not defined directly in terms of
`rTensorHomToHomRTensor`, but the equivalence between the two is given by
`rTensorHomEquivHomRTensor_toLinearMap` and `rTensorHomEquivHomRTensor_apply`. -/
noncomputable def rTensorHomEquivHomRTensor : (M →ₗ[R] P) ⊗[R] Q ≃ₗ[R] M →ₗ[R] P ⊗[R] Q :=
congr (dualTensorHomEquiv R M P).symm (LinearEquiv.refl R Q) ≪≫ₗ TensorProduct.assoc R _ P Q ≪≫ₗ
dualTensorHomEquiv R M _
