Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-03 15:25 e4ee18b8

View on Github →

feat(category_theory/adjunction): additional simp lemmas (#1143)

feat(category_theory/adjunction): additional simp lemmas
spaces Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

Modified src/category_theory/adjunction/basic.lean

added theorem category_theory.adjunction.counit_naturality

added theorem category_theory.adjunction.counit_naturality_assoc

added theorem category_theory.adjunction.left_triangle_components_assoc

added theorem category_theory.adjunction.right_triangle_components_assoc

added theorem category_theory.adjunction.unit_naturality

added theorem category_theory.adjunction.unit_naturality_assoc