English
There is a natural linear equivalence between the tensor of duals and the dual of the tensor using a chosen basis, providing a canonical dualDistribEquivOfBasis.
Русский
Существует естественное линейное эквивалентное отображение между тензором двойственных пространств и двойственным тензором через выбранный базис, задающее канонический dualDistribEquivOfBasis.
LaTeX
$$$$ dualDistribEquivOfBasis\\ (b,c) : Dual_R M \\otimes_R Dual_R N \\simeq_\\ell Dual_R (M \\otimes_R N). $$$$
Lean4
/-- A linear equivalence between `Dual M ⊗ Dual N` and `Dual (M ⊗ N)` when `M` and `N` are finite free
modules. It sends `f ⊗ g` to the composition of `TensorProduct.map f g` with the natural
isomorphism `R ⊗ R ≃ R`.
-/
@[simp]
noncomputable def dualDistribEquiv : Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N) :=
dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N)
