Commit 2023-05-09 10:06 98de1337

View on Github →

feat: port CategoryTheory.Preadditive.InjectiveResolution (#3860)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Preadditive/InjectiveResolution.lean

added theorem CategoryTheory.InjectiveResolution.complex_d_comp

added def CategoryTheory.InjectiveResolution.self

added theorem CategoryTheory.InjectiveResolution.ι_f_succ

added theorem CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d

added structure CategoryTheory.InjectiveResolution