Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes