mathlib

01af73ae - feat(alegbra/homology/short_exact/abelian.lean): Right split exact sequences + case of modules (#14376)

feat(alegbra/homology/short_exact/abelian.lean): Right split exact sequences + case of modules (#14376) A right split short exact sequence in an abelian category is split. Also, in the case of the Module category, a version fully expressed in terms of modules and linear maps is provided.