Theorem CommRingCat.coproductCocone_inr

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.coproductCocone_inrView on Github →