mathlib3
chore(category_theory/notation): consistently use notation for functor.id
#1378

Merged

chore(category_theory/notation): consistently use notation for functor.id #1378

mergify merged 5 commits into master from functor_id_notation

chore(category_theory/notation): consistently use notation for functo…

75b5ea07

kim-em requested a review from

jcommelin 6 years ago

kim-em requested a review 6 years ago

jcommelin approved these changes on 2019-09-01

jcommelin added ready-to-merge

oops, overzealous search-and-replace

8bc2ffe9

fa7f5069

69f521ff

0e064d5c

mergify merged 6d2b3ed8 into master 6 years ago

mergify deleted the functor_id_notation branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone