Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-28 13:31 3837abcb

View on Github →

feat(data/list/*): subperm_singleton_iff (#11680)

Estimated changes

Modified src/data/list/count.lean

modified theorem list.count_pos

added theorem list.one_le_count_iff_mem

Modified src/data/list/perm.lean

added theorem list.subperm_singleton_iff