Grothendieck groups by presentation #
GrothendieckPresentation is generic in its generator and relation types — it
mentions no category at all — and K₀Ab instantiates it at the short exact
sequences of an abelian category.
Neither file uses anything triangulated, which is why they live here rather than
under Triangulated/. The triangulated instantiation K₀, built on
distinguished triangles, stays at Triangulated/GrothendieckGroup/ where it
belongs.