Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-02-10 21:01
db0fa613
View on Github →
feat(category_theory/differential_object): the shift functor (
#6111
) Requested by @jcommelin.
Estimated changes
Modified
src/category_theory/differential_object.lean
added
def
category_theory.differential_object.shift_counit
added
def
category_theory.differential_object.shift_counit_inv
added
def
category_theory.differential_object.shift_counit_iso
added
def
category_theory.differential_object.shift_functor
added
def
category_theory.differential_object.shift_inverse
added
def
category_theory.differential_object.shift_inverse_obj
added
def
category_theory.differential_object.shift_unit
added
def
category_theory.differential_object.shift_unit_inv
added
def
category_theory.differential_object.shift_unit_iso