Theorem CategoryTheory.Splitting.π_section_eq_id_sub

Modification history

2023-12-21 16:16

Mathlib/Algebra/Homology/ShortExact/Preadditive.lean

refactor: use the new homology API for the four and the five lemmas (#9022) …

Deleted CategoryTheory.Splitting.π_section_eq_id_sub View on Github →

2023-04-24 12:12

Mathlib/Algebra/Homology/ShortExact/Preadditive.lean

feat: port Algebra.Homology.ShortExact.Preadditive (#3611)

Added CategoryTheory.Splitting.π_section_eq_id_sub View on Github →