…and map for the tensor product of dual space (#32613)

Constructs a basis for `PiTensorProduct` given bases for the component spaces and defines maps between the tensor product of dual spaces and the dual of a tensor product.

Main definitions:
* `Basis.piTensorProduct`: Given bases `b : Π i, Basis (κ i) R (M i)` for each component space `M i`, constructs a basis for `⨂[R] i, M i` indexed by `Π i, κ i` defined by sending `p : Π i, κ i` to `⨂ₜ[R] i, (b i) (p i)`.

* `PiTensorProduct.dualDistrib`: The canonical linear map from `⨂[R] i, Dual R (M i)` to
  `Dual R (⨂[R] i, M i)`, sending `⨂ₜ[R] i, f i` to the composition of
  `PiTensorProduct.map f` with the linear equivalence `⨂[R] i, R →ₗ R` given by multiplication.

* `PiTensorProduct.dualDistribEquiv`: A linear equivalence between `⨂[R] i, Dual R (M i)`
  and `Dual R (⨂[R] i, M i)` when all `M i` are finite free modules. If
  `f : (i : ι) → Dual R (M i)`, then this equivalence sends `⨂ₜ[R] i, f i` to the composition of
  `PiTensorProduct.map f` with the natural isomorphism `⨂[R] i, R ≃ R` given by multiplication.

- [x] depends on: #32456