Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-04 19:35 178c09d7

View on Github →

feat(natural_isomorphism): componentwise isos are isos (#671)

Estimated changes

Modified src/category_theory/isomorphism.lean

added theorem category_theory.is_iso.hom_inv_id

deleted def category_theory.is_iso.hom_inv_id

added theorem category_theory.is_iso.hom_inv_id_assoc

added theorem category_theory.is_iso.inv_hom_id

deleted def category_theory.is_iso.inv_hom_id

added theorem category_theory.is_iso.inv_hom_id_assoc

Modified src/category_theory/natural_isomorphism.lean