Commit 2022-05-30 13:47 01af73ae
View on Github →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.