English
TensorProduct.map applied to two dualTensorHom instances equals a single dualTensorHom on a product.
Русский
Применение TensorProduct.map к двум dualTensorHom-образованиям равно одному dualTensorHom на произведении модулей.
LaTeX
$$$\mathrm{TensorProduct}.map (\mathrm{dualTensorHom} R M P (f \otimes p)) (\mathrm{dualTensorHom} R N Q (g \otimes q)) = \\ \mathrm{dualTensorHom}(R, M \otimes N, P \otimes Q)(\mathrm{dualDistrib}(R M N)(f \otimes g) \otimes (p \otimes q)).$$$
Lean4
/-- If `M` is finite free, the natural map $M^* ⊗ N → Hom(M, N)$ is an
equivalence. -/
@[simp]
noncomputable def dualTensorHomEquiv : Module.Dual R M ⊗[R] N ≃ₗ[R] M →ₗ[R] N :=
dualTensorHomEquivOfBasis (Module.Free.chooseBasis R M)
