Commit 2024-12-20 12:18 5ba57828
View on Github →feat(Algebra/Category/Ring): Tensor product over Z is coproduct in CommRingCat (#19976)
Show that the tensor product over the integers is a coproduct in the category of commutative rings. This is needed for constructing a ChosenFiniteProducts instance for the category of affine schemes. It would be nice to have the more general statement for commutative R-algebras, but it seems like mathlib does not define the category of commutative R-algebras yet.