Skip to content

Instantly share code, notes, and snippets.

@solson

solson/fintype.lean

Created May 10, 2018 06:18
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save solson/7a16f92c0bf22ed944cdcd4cd8548106 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save solson/7a16f92c0bf22ed944cdcd4cd8548106 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
fintype.lean
@[simp] theorem card_prod : card (α × β) = card α * card β := by simp [fintype.values]
@[simp] theorem card_sum : card (α ⊕ β) = card α + card β := by simp [fintype.values]
@[simp] theorem card_empty_prod : card (empty × α) = 0 := by simp [fintype.values]
@[simp] theorem card_prod_empty : card (α × empty) = 0 := by simp [fintype.values]
@[simp] theorem card_empty_sum : card (empty ⊕ α) = card α := by simp [fintype.values]
@[simp] theorem card_sum_empty : card (α ⊕ empty) = card α := by simp [fintype.values]
@[simp] theorem card_unit_prod : card (unit × α) = card α := by simp [fintype.values]
@[simp] theorem card_prod_unit : card (α × unit) = card α := by simp [fintype.values]
@[simp] theorem card_option : card (option α) = 1 + card α := by simp [fintype.values]
theorem card_sum_eq_card_prod : card (α ⊕ α) = card (bool × α) := by simp [card, fintype.values]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment