Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 07:36 ef377a92

View on Github →

chore(data/list/sort): docs, add a few lemmas (#5274)

  • Add a module docstring and section headers.
  • Rename list.eq_of_sorted_of_perm to list.eq_of_perm_of_sorted; the new name reflects the order of arguments.
  • Add a few lemmas.

Estimated changes

deleted theorem list.eq_of_sorted_of_perm
modified theorem list.length_merge_sort
modified theorem list.merge_sort_eq_self
modified theorem list.perm_insertion_sort
modified theorem list.perm_merge
modified theorem list.perm_merge_sort
modified theorem list.perm_ordered_insert
added theorem list.sorted.merge
modified theorem list.sorted_insertion_sort
deleted theorem list.sorted_merge
modified theorem list.sorted_merge_sort