Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-02 07:10 d94f0a27

View on Github →

chore(data/list): a list sorted w.r.t. (<) has no duplicates (#5550)

Estimated changes

Modified src/data/list/nodup.lean

Modified src/data/list/sort.lean

Modified src/order/rel_classes.lean

added theorem ne_of_irrefl