Mathlib v3 is deprecated. Go to Mathlib v4

Theorem category_theory.nat_iso.hom_app_inv_app_id

Modification history

2020-07-14 15:06
src/category_theory/natural_isomorphism.lean
chore(category_theory/natural_isomorphism): move lemmas to correct namespace, add simp lemma (#3401)
Deleted category_theory.nat_iso.hom_app_inv_app_idView on Github →
2020-03-03 11:51
src/category_theory/natural_isomorphism.lean
feat(tactic/lint): check for redundant simp lemmas (#2066) …
Modified category_theory.nat_iso.hom_app_inv_app_idView on Github →
2018-11-28 04:36
category_theory/natural_isomorphism.lean
feat(category_theory/equivalence): equivalences, slice tactic (#479)
Added category_theory.nat_iso.hom_app_inv_app_idView on Github →