Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-05-03 14:41 ef43edfd

View on Github →

feat(data/finset): add list.to_finset theorems

Estimated changes

Modified data/finset.lean

added theorem list.to_finset_card_of_nodup

added theorem list.to_finset_cons

added theorem list.to_finset_nil

Modified data/list/basic.lean

added theorem list.erase_dup_idempotent

added theorem list.pw_filter_idempotent