…`, `DFinsupp`, and `DirectSum` (#32456)

Adds linear equivalences for `PiTensorProduct`s taken over `Finsupp`, `DFinsupp`, and `DirectSum`. The main definitions are:
* `PiTensorProduct.ofDFinsuppEquiv` is the linear equivalence of tensor products over `DFinsupp` to a `DFinsupp` of tensor products
* `PiTensorProduct.ofFinsuppEquiv` is the linear equivalence of tensor products over `Finsupp` to a `Finsupp` of tensor products
* `PiTensorProduct.ofDirectSumEquiv` is the linear equivalence of tensor products over a direct sum to the direct sum over tensor products

…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