chore: fix name of List.length_mergeSort (#5373)

leanprover · Sep 17, 2024 · 21d71de · 21d71de
1 parent b74f85a
commit 21d71de
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
@@ -234,7 +234,7 @@ theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l
         (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
 termination_by l => l.length
 
-@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length :=
+@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length :=
   (mergeSort_perm l le).length_eq
 
 @[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort l le ↔ a ∈ l :=