Mathlib Changelog
v4
Changelog
About
Github
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