Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-08 20:06 3399baa9

View on Github →

feat(data/encodable): ported data/encodable.lean from Lean2

Estimated changes

Created data/encodable.lean

added def encodable_of_equiv

added def encodable_of_left_injection

added theorem succ_ne_zero

Modified data/list/sort.lean

added theorem list.eq_of_sorted_of_perm

deleted theorem list.sorted_insert_sort

added theorem list.sorted_insertion_sort