mathlib3
chore(category_theory/functor_category): improve comment warning about hcomp_assoc [ci skip]
#1434
Merged
Overview
Commits
3
Changes
View On GitHub

chore(category_theory/functor_category): improve comment warning about hcomp_assoc [ci skip] #1434

mergify merged 3 commits into master from hcomp_comment
kim-em
kim-em expanding comment
542afdaf
kim-em no scare quotes
ea9cd14e
kim-em kim-em requested a review 6 years ago
rwbarton
rwbarton approved these changes on 2019-09-11
rwbarton rwbarton changed the title chore(category_theory/functor_category): improve comment warning about hcomp_assoc chore(category_theory/functor_category): improve comment warning about hcomp_assoc [ci skip] 6 years ago
rwbarton rwbarton added ready-to-merge
mergify[bot] Merge branch 'master' into hcomp_comment
f4fd1aa6
mergify mergify merged 590fb896 into master 6 years ago
mergify mergify deleted the hcomp_comment branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum