Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-19 13:17 d9102835

View on Github →

chore(category_theory/endomorphism): make map_End and map_Aut use bundled homs (#1461)

Migrate functor.map_End and functor.map_Aut to bundled homs Adjust implicit arguments of iso.ext
Add docstrings

Estimated changes

Modified src/category_theory/endomorphism.lean

modified def category_theory.functor.map_Aut

modified def category_theory.functor.map_End

Modified src/category_theory/isomorphism.lean

added theorem category_theory.functor.map_iso_refl

modified theorem category_theory.iso.ext

modified theorem category_theory.iso.self_symm_id

modified theorem category_theory.iso.symm_self_id