mathlib

69b2e97a - chore(ring_theory/tensor_product): replace `is_scalar_tower` by `smul_comm_class` in `left_algebra` (#19118)

chore(ring_theory/tensor_product): replace `is_scalar_tower` by `smul_comm_class` in `left_algebra` (#19118) With this change, this instance works for both restriction (e.g tensor product over `ℂ` of complex algebras is a real algebra) and extension (e.g tensor product over `ℝ` of complex algebras is a complex algebra) of scalars. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Tensor.20products) I also removes [algebra.tensor_product.tensor_product.is_scalar_tower](https://leanprover-community.github.io/mathlib_docs/ring_theory/tensor_product.html#algebra.tensor_product.tensor_product.is_scalar_tower) since it is automatically inferred from [tensor_product.is_scalar_tower](https://leanprover-community.github.io/mathlib_docs/linear_algebra/tensor_product.html#tensor_product.is_scalar_tower) Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>