File tree Expand file tree Collapse file tree 1 file changed +0
-5
lines changed
Expand file tree Collapse file tree 1 file changed +0
-5
lines changed Original file line number Diff line number Diff line change @@ -25,27 +25,22 @@ namespace List
2525
2626variable {α : Type u}
2727
28-
29- @[simp]
3028theorem finRange_eq_nil {n : ℕ} : finRange n = [] ↔ n = 0 := by
3129 rw [← length_eq_zero_iff, length_finRange]
3230
3331@[simp]
3432lemma count_finRange {n : ℕ} (a : Fin n) : count a (finRange n) = 1 := by
3533 simp [List.Nodup.count (nodup_finRange n)]
3634
37- @[simp]
3835theorem finRange_map_get (l : List α) : (finRange l.length).map l.get = l :=
3936 List.ext_get (by simp) (by simp)
4037
41- @[simp]
4238theorem finRange_map_getElem (l : List α) : (finRange l.length).map (l[·.1 ]) = l :=
4339 finRange_map_get l
4440
4541@[simp] theorem idxOf_finRange {k : ℕ} (i : Fin k) : (finRange k).idxOf i = i := by
4642 simpa using (nodup_finRange k).idxOf_getElem i
4743
48- @[simp]
4944theorem map_coe_finRange (n : ℕ) : ((finRange n) : List (Fin n)).map (Fin.val) = List.range n := by
5045 apply List.ext_getElem <;> simp
5146
You can’t perform that action at this time.
0 commit comments