Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-18 19:04 e4bf4960

View on Github →

feat(data/set/finite): simple infiniteness lemmas (#9242)

Estimated changes

Modified archive/imo/imo2008_q2.lean

Modified src/algebra/big_operators/finprod.lean

Modified src/data/set/finite.lean

added theorem set.infinite.diff

added theorem set.infinite.exists_nat_lt

added theorem set.infinite.exists_not_mem_finset

deleted theorem set.infinite_mono

Modified src/data/set/intervals/infinite.lean

Modified src/ring_theory/polynomial/dickson.lean