The category of commutative rings has all colimits.

This file uses a "pre-automated" approach, just as for Mon/colimits.lean. It is a very uniform approach, that conceivably could be synthesised directly by a tactic that analyses the shape of comm_ring and ring_hom.