mathlib3
chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset
#1615
Merged
Merged
chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset #1615
mergify
merged
5 commits into
master
from
move-fintype_of_finset
chore(data/set/finite): move defns up hierarchy
a724ca26
get namespaces right
d435ff8b
fixes
63f5834b
robertylewis
commented
on 2019-10-28
robertylewis
changed the title 
ChrisHughes24
approved these changes
on 2019-10-31
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into move-fintype_of_finset
cc2d0916
fix build
3591e72a
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub