finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset (#1615)

Commit

6 years ago

chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset (#1615) * chore(data/set/finite): move defns up hierarchy * get namespaces right * fixes * fix build

References

#1615 - chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset

Author

kim-em

Committer

mergify[bot]

Parents

6b51787e

mathlib cd0bc32b - chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset (#1615)

mathlib
cd0bc32b - chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset (#1615)