mathlib
2b6b9ffc
- feat(category_theory/abelian/derived): add left_derived_zero_iso_self (#12403)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(category_theory/abelian/derived): add left_derived_zero_iso_self (#12403) We add `left_derived_zero_iso_self`: the natural isomorphism `(F.left_derived 0) ≅ F` if `preserves_finite_colimits F`. From lean-liquid Co-authored-by: @adamtopaz
Author
riccardobrasca
Parents
4c60258c
Loading