Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-07 14:30 51452619

View on Github →

feat(data/fintype/list): induced fintype on nodup lists (#8171)

Estimated changes

Created src/data/fintype/list.lean

added def multiset.lists

added theorem multiset.lists_coe

added theorem multiset.mem_lists_iff

Modified src/data/list/cycle.lean

added def cycle.decidable_nontrivial_coe

added theorem cycle.nodup.nontrivial_iff

added theorem cycle.nontrivial_coe_nodup_iff