Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-02 17:36 68c98eb7

View on Github →

feat(category_theory/isomorphism): lemmas for manipulating isomorphisms

Estimated changes

Modified category_theory/equivalence.lean

Modified category_theory/isomorphism.lean

added theorem category_theory.iso.comp_inv_eq

added theorem category_theory.iso.eq_comp_inv

added theorem category_theory.iso.eq_inv_comp

added theorem category_theory.iso.hom_inv_id_assoc

added theorem category_theory.iso.inv_comp_eq

added theorem category_theory.iso.inv_hom_id_assoc

Modified category_theory/natural_isomorphism.lean