Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-14 15:06 6c1ae3b1

View on Github →

chore(category_theory/natural_isomorphism): move lemmas to correct namespace, add simp lemma (#3401)

Estimated changes

Modified src/category_theory/closed/cartesian.lean

Modified src/category_theory/equivalence.lean

Modified src/category_theory/limits/cones.lean

Modified src/category_theory/limits/limits.lean

Modified src/category_theory/natural_isomorphism.lean

modified def category_theory.iso.app

added theorem category_theory.iso.hom_inv_id_app

added theorem category_theory.iso.inv_hom_id_app

deleted theorem category_theory.nat_iso.hom_app_inv_app_id

deleted theorem category_theory.nat_iso.hom_inv_id_app

deleted theorem category_theory.nat_iso.inv_app_hom_app_id

deleted theorem category_theory.nat_iso.inv_hom_id_app

Modified src/category_theory/opposites.lean

Modified src/category_theory/types.lean

added theorem category_theory.functor_to_types.hom_inv_id_app_apply

added theorem category_theory.functor_to_types.inv_hom_id_app_apply