Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-29 08:42 79880e86

View on Github →

chore(data/fintype/intervals): simp Ico_*_card lemmas (#2271)

Estimated changes

Modified src/data/finset.lean

added theorem finset.Ico_ℤ.card

Modified src/data/fintype/intervals.lean

added theorem set.Ico_pnat_card

added theorem set.Ico_ℕ_card

added theorem set.Ico_ℤ_card

Modified src/data/pnat/intervals.lean

added theorem pnat.Ico.card