theorem Fin.foldlM_eq_foldlM_finRange {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin n → m α) (x : α) : Fin.foldlM n f x = List.foldlM f x (List.finRange n)

@[deprecated Fin.foldlM_eq_foldlM_finRange]

theorem Fin.foldlM_eq_foldlM_list {m : Type u_1 → Type u_2} {α : Type u_1} {n : Nat} [Monad m] (f : α → Fin n → m α) (x : α) : Fin.foldlM n f x = List.foldlM f x (List.finRange n)

Alias of Fin.foldlM_eq_foldlM_finRange.

theorem Fin.foldrM_eq_foldrM_finRange {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) : Fin.foldrM n f x = List.foldrM f x (List.finRange n)

@[deprecated Fin.foldrM_eq_foldrM_finRange]

theorem Fin.foldrM_eq_foldrM_list {m : Type u_1 → Type u_2} {n : Nat} {α : Type u_1} [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x : α) : Fin.foldrM n f x = List.foldrM f x (List.finRange n)

Alias of Fin.foldrM_eq_foldrM_finRange.

theorem Fin.foldl_eq_foldl_finRange {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldl n f x = List.foldl f x (List.finRange n)

@[deprecated Fin.foldl_eq_foldl_finRange]

theorem Fin.foldl_eq_foldl_list {α : Type u_1} {n : Nat} (f : α → Fin n → α) (x : α) : Fin.foldl n f x = List.foldl f x (List.finRange n)

Alias of Fin.foldl_eq_foldl_finRange.

theorem Fin.foldr_eq_foldr_finRange {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : Fin.foldr n f x = List.foldr f x (List.finRange n)

@[deprecated Fin.foldr_eq_foldr_finRange]

theorem Fin.foldr_eq_foldr_list {n : Nat} {α : Type u_1} (f : Fin n → α → α) (x : α) : Fin.foldr n f x = List.foldr f x (List.finRange n)

Alias of Fin.foldr_eq_foldr_finRange.