mathlib

4977fd9d - feat(ring_theory/finiteness): tensor product of two finite modules is finite (#13733)

feat(ring_theory/finiteness): tensor product of two finite modules is finite (#13733) Removes [finite_dimensional_tensor_product](https://leanprover-community.github.io/mathlib_docs/linear_algebra/tensor_product_basis.html#finite_dimensional_tensor_product) since it's now proved by `infer_instance`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>