Theorem CommRingCat.coproductCocone_inl

Modification history

2025-07-26 23:35
Mathlib/Algebra/Category/Ring/Constructions.lean
chore: more indentation fixes (#27502) …
Modified CommRingCat.coproductCocone_inlView on Github →
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_inlView on Github →