Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-15 10:26 3d512f79

View on Github →

chore(category_theory/isomorphism): docstring, DRY, add some trivial lemmas (#1309)

add module docstring;
use as_iso more aggressively to avoid repeating proofs;
add more trivial lemmas.

Estimated changes

Modified src/category_theory/isomorphism.lean

modified def category_theory.as_iso

modified theorem category_theory.functor.map_inv

added theorem category_theory.functor.map_iso_symm

deleted def category_theory.inv

modified theorem category_theory.is_iso.hom_inv_id

modified theorem category_theory.is_iso.hom_inv_id_assoc

modified theorem category_theory.is_iso.inv_comp

modified theorem category_theory.is_iso.inv_hom_id

modified theorem category_theory.is_iso.inv_hom_id_assoc

modified theorem category_theory.is_iso.inv_id

modified theorem category_theory.is_iso.is_iso.inv_inv

modified theorem category_theory.is_iso.iso.inv_hom

modified theorem category_theory.is_iso.iso.inv_inv

modified theorem category_theory.iso.refl_symm

added theorem category_theory.iso.refl_trans

added theorem category_theory.iso.self_symm_id

added theorem category_theory.iso.self_symm_id_assoc

added theorem category_theory.iso.symm_eq_iff

added theorem category_theory.iso.symm_self_id

added theorem category_theory.iso.symm_self_id_assoc

added theorem category_theory.iso.symm_symm_eq

added theorem category_theory.iso.trans_assoc

added theorem category_theory.iso.trans_refl

modified theorem category_theory.iso.trans_symm