Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-27 22:43 ccd895f8

View on Github →

feat(category_theory/types): conversions between iso and equiv

Estimated changes

Modified src/category_theory/types.lean

added def category_theory.iso.to_equiv

added theorem category_theory.iso.to_equiv_fun

added theorem category_theory.iso.to_equiv_symm_fun

added def equiv.to_iso

added theorem equiv.to_iso_hom

added theorem equiv.to_iso_inv