@[simp]

theorem List.length_finRange (n : Nat) : (List.finRange n).length = n

@[deprecated List.length_finRange]

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

Alias of List.length_finRange.

@[simp]

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

@[deprecated List.getElem_finRange]

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

Alias of List.getElem_finRange.

@[simp]

theorem List.finRange_zero : List.finRange 0 = []

@[deprecated List.finRange_zero]

theorem List.list_zero : List.finRange 0 = []

Alias of List.finRange_zero.

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

@[deprecated List.finRange_succ]

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

Alias of List.finRange_succ.

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

@[deprecated List.finRange_succ_last]

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

Alias of List.finRange_succ_last.

theorem List.finRange_reverse (n : Nat) : (List.finRange n).reverse = List.map Fin.rev (List.finRange n)

@[deprecated List.finRange_reverse]

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

Alias of List.finRange_reverse.