Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-25 18:32 b6e6c84f

View on Github →

feat(data/finset/basic): to_list (#8797) Produce a list of the elements of a finite set using choice.

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.coe_to_list

added theorem finset.length_to_list

added theorem finset.mem_to_list

added theorem finset.nodup_to_list

added theorem finset.to_list_empty

added theorem finset.to_list_to_finset

Modified src/data/finset/sort.lean

added theorem finset.sort_perm_to_list