@[deprecated List.length_finRange (since := "2024-11-19")]

theorem List.length_list {n : Nat} : (finRange n).length = n

Alias of List.length_finRange.

@[deprecated List.getElem_finRange (since := "2024-11-19")]

theorem List.getElem_list {n i : Nat} (h : i < (finRange n).length) : (finRange n)[i] = Fin.cast ⋯ ⟨i, h⟩

Alias of List.getElem_finRange.

@[deprecated List.finRange_zero (since := "2024-11-19")]

theorem List.list_zero : finRange 0 = []

Alias of List.finRange_zero.

@[deprecated List.finRange_succ (since := "2024-11-19")]

theorem List.list_succ {n : Nat} : finRange (n + 1) = 0 :: map Fin.succ (finRange n)

Alias of List.finRange_succ.

@[deprecated List.finRange_succ_last (since := "2024-11-19")]

theorem List.list_succ_last {n : Nat} : finRange (n + 1) = map Fin.castSucc (finRange n) ++ [Fin.last n]

Alias of List.finRange_succ_last.

@[deprecated List.finRange_reverse (since := "2024-11-19")]

theorem List.list_reverse {n : Nat} : (finRange n).reverse = map Fin.rev (finRange n)

Alias of List.finRange_reverse.