Def CommRingCat.coproductCoconeIsColimit

Modification history

2024-12-20 12:18

Mathlib/Algebra/Category/Ring/Constructions.lean

feat(Algebra/Category/Ring): Tensor product over Z is coproduct in `CommRingCat` (#19976) …

Added CommRingCat.coproductCoconeIsColimit View on Github →