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

Commits
  • Define equivalence between `{ f // is_monoid_hom f }` and `monoid_hom`
    urkud committed 7 years ago
  • Migrate `single_obj` to bundled homomorphisms
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 7 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 6 years ago
  • Fix `Mon.hom_equiv_monoid_hom` as suggested by @jcommelin
    urkud committed 6 years ago
  • Merge branch 'master' into single-obj-bundled
    urkud committed 6 years ago
  • Merge branch 'master' into single-obj-bundled
    mergify[bot] committed 6 years ago
Loading