Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-09 22:27 60e4bb92

View on Github →

refactor(category_theory/endomorphism): move to a dedicated file; prove simple lemmas (#1195)

  • Move definitions of End and Aut to a dedicated file
  • Adjust some proofs, use namespace, add docstrings
  • and functor.map_iso define homomorphisms of End/Aut
  • Define functor.map_End and functor.map_Aut

Estimated changes