Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-01 12:58 7cbca35f

View on Github →

feat(data/fintype/intervals): fintype instances for set.{Icc,Ioc,Ioo} (#8123)

Estimated changes

Modified src/data/fintype/intervals.lean

added theorem set.Icc_ℤ_card

modified theorem set.Icc_ℤ_finite

added theorem set.Ioc_ℤ_card

modified theorem set.Ioc_ℤ_finite

added theorem set.Ioo_ℤ_card

modified theorem set.Ioo_ℤ_finite