Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:44 1d2eda7b

View on Github →

feat(category_theory/isomorphism): as_iso Also clean up some proofs.

Estimated changes

Modified src/category_theory/isomorphism.lean

added def category_theory.as_iso

added theorem category_theory.as_iso_hom

added theorem category_theory.as_iso_inv

modified def category_theory.functor.on_iso

modified theorem category_theory.iso.ext