Mathlib v3 is deprecated. Go to Mathlib v4

Theorem CommRing.pushout_cocone_X

Modification history

2021-12-07 15:39
src/algebra/category/CommRing/constructions.lean
feat(algebra/category): (co)limits in CommRing (#10593)
Modified CommRing.pushout_cocone_XView on Github →
2021-11-17 07:06
src/algebra/category/CommRing/pushout.lean
lint(*): curly braces linter (#10280) …
Modified CommRing.pushout_cocone_XView on Github →
2021-09-24 00:26
src/algebra/category/CommRing/pushout.lean
feat(algebra/*): Tensor product is the fibered coproduct in CommRing (#9338)
Added CommRing.pushout_cocone_XView on Github →