Theorem CategoryTheory.Abelian.factorThruImage_comp_coimageIsoImage'_inv

Modification history