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