Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-28 21:31 3b195032

View on Github →

refactor(category_theory/single_obj): migrate to bundled morphisms (#1330)

  • Define equivalence between { f // is_monoid_hom f } and monoid_hom
  • Migrate single_obj to bundled homomorphisms Fix a bug in to_End: the old implementation used a wrong monoid structure on End.
  • Fix Mon.hom_equiv_monoid_hom as suggested by @jcommelin

Estimated changes