Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-23 10:17 8b9a47b6

View on Github →

feat(data/finset/basic): finset.exists_ne_of_one_lt_card (#8816) Analog of fintype.exists_ne_of_one_lt_card.

Estimated changes