mathlib

ae6bf562 - feat(ring_theory/tensor_product): tensor product of algebras (#3050)

feat(ring_theory/tensor_product): tensor product of algebras (#3050) The R-algebra structure on the tensor product of two R-algebras. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>