Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-31 21:03 cd0bc32b

View on Github →

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

Estimated changes

added theorem fintype.card_of_finset
added theorem set.mem_to_finset
added theorem set.mem_to_finset_val
added def set.to_finset
deleted theorem set.mem_to_finset
deleted theorem set.mem_to_finset_val
deleted def set.to_finset