PR #2101 feat(category_theory): images in Ab and Type

feat(category_theory): images in Ab and Type #2101

mergify merged 16 commits into master from images_in_Ab

kim-em added blocked-by-other-PR

cipher1024 assigned

jcommelin 6 years ago

bryangingechen removed blocked-by-other-PR

kim-em added awaiting-review

jcommelin added blocked-by-other-PR

not stacked on top of limits/colimits

bbaf893b

kim-em force pushed from f1eae483 to bbaf893b 6 years ago

kim-em removed blocked-by-other-PR

comment

308ccbee

add ext to add_monoid_hom.ext

43420e00

jcommelin removed awaiting-review

jcommelin commented on 2020-03-13

fix

5313c9d5

cleanup

92600a07

merge

4ed03e45

suggestions from review

87d5bf36

Merge remote-tracking branch 'origin/master' into images_in_Ab

474d882d

kim-em added awaiting-review

Merge remote-tracking branch 'origin/master' into images_in_Ab

d0bd2c71

fix

fd58a4b0

jcommelin approved these changes on 2020-03-16

use more existing structure

4e90f914

kim-em requested a review from

jcommelin 6 years ago

merge

5f47d3b5

fix names

dbcc9c72

jcommelin approved these changes on 2020-03-17

jcommelin removed awaiting-review

jcommelin added ready-to-merge

oops

905ad173

linter

5fc4dc0b

Merge branch 'master' into images_in_Ab

67014a94

mergify merged f07a1ebf into master 6 years ago

mergify deleted the images_in_Ab branch 6 years ago

Reviewers

jcommelin

Assignees

jcommelin

Labels

ready-to-merge

Milestone

No milestone

mathlib3 feat(category_theory): images in Ab and Type #2101 Merged

feat(category_theory): images in Ab and Type #2101

mathlib3
feat(category_theory): images in Ab and Type
#2101

Merged