mathlib3
chore(category_theory/concrete_category): take an instance, rather than extending, category
#2195
Merged
Merged
chore(category_theory/concrete_category): take an instance, rather than extending, category #2195
mergify
merged
12 commits into
master
from
concrete_no_extend
chore(category_theory/concrete_category): take an instance, rather th…
1961b61f
jcommelin
commented
on 2020-03-19
use large_category
54b962eb
fixes
e638e0f6
jcommelin
commented
on 2020-03-19
fixes
0946e322
fix
072e9909
fix
569021f7
typo
1b63d573
jcommelin
approved these changes
on 2020-04-01
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into concrete_no_extend
54adcc0a
Merge branch 'master' into concrete_no_extend
3b5ecb50
update
dd9855e8
update
aeb3ac1e
Merge branch 'master' into concrete_no_extend
afb39e45
Login to write a write a comment.
Login via GitHub