Commit 2023-06-02 09:01 69b2e97a

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 I also removes algebra.tensor_product.tensor_product.is_scalar_tower since it is automatically inferred from tensor_product.is_scalar_tower