Commit 2024-03-02 20:50 fb2570a4
View on Github →feat(LinearAlgebra/PiTensorProduct): arbitrary tensor product of algebras (#9395) Let $R$ be a commutative ring and $(A_i)$ a bunch of $R$-algebras, then $\bigotimes_{R} A$ is an $R$-algebra as well. In particular, taking $R$ to be $\mathbb{Z}$, we get tensor product of rings