mathlib documentation

data.list.range

@[simp]
theorem list.length_range' (s n : ) :

@[simp]
theorem list.range'_eq_nil {s n : } :

@[simp]
theorem list.mem_range' {m s n : } :
m list.range' s n s m m < s + n

theorem list.map_add_range' (a s n : ) :

theorem list.map_sub_range' (a s n : ) :
a slist.map (λ (x : ), x - a) (list.range' s n) = list.range' (s - a) n

theorem list.chain_succ_range' (s n : ) :
list.chain (λ (a b : ), b = a.succ) s (list.range' (s + 1) n)

theorem list.nodup_range' (s n : ) :

@[simp]
theorem list.range'_append (s m n : ) :
list.range' s m ++ list.range' (s + m) n = list.range' s (n + m)

theorem list.nth_range' (s : ) {m n : } :
m < n(list.range' s n).nth m = some (s + m)

theorem list.range'_concat (s n : ) :
list.range' s (n + 1) = list.range' s n ++ [s + n]

@[simp]
theorem list.length_range (n : ) :

@[simp]
theorem list.range_eq_nil {n : } :

theorem list.nodup_range (n : ) :

@[simp]
theorem list.mem_range {m n : } :

@[simp]
theorem list.not_mem_range_self {n : } :

@[simp]
theorem list.self_mem_range_succ (n : ) :
n list.range (n + 1)

theorem list.nth_range {m n : } :
m < n(list.range n).nth m = some m

@[simp]
theorem list.length_iota (n : ) :

theorem list.nodup_iota (n : ) :

theorem list.mem_iota {m n : } :
m list.iota n 1 m m n

theorem list.reverse_range' (s n : ) :
(list.range' s n).reverse = list.map (λ (i : ), s + n - 1 - i) (list.range n)

def list.fin_range (n : ) :
list (fin n)

All elements of fin n, from 0 to n-1.

Equations
@[simp]
theorem list.mem_fin_range {n : } (a : fin n) :

@[simp]

@[simp]

theorem list.prod_range_succ {α : Type u} [monoid α] (f : → α) (n : ) :

theorem list.sum_range_succ {α : Type u} [add_monoid α] (f : → α) (n : ) :

theorem list.prod_range_succ' {α : Type u} [monoid α] (f : → α) (n : ) :
(list.map f (list.range n.succ)).prod = (f 0) * (list.map (λ (i : ), f i.succ) (list.range n)).prod

A variant of prod_range_succ which pulls off the first term in the product rather than the last.

theorem list.sum_range_succ' {α : Type u} [add_monoid α] (f : → α) (n : ) :
(list.map f (list.range n.succ)).sum = f 0 + (list.map (λ (i : ), f i.succ) (list.range n)).sum

A variant of sum_range_succ which pulls off the first term in the sum rather than the last.

@[simp]
theorem list.enum_from_map_fst {α : Type u} (n : ) (l : list α) :

@[simp]
theorem list.enum_map_fst {α : Type u} (l : list α) :

@[simp]
theorem list.nth_le_range {n : } (i : ) (H : i < (list.range n).length) :
(list.range n).nth_le i H = i

theorem list.of_fn_eq_pmap {α : Type u_1} {n : } {f : fin n → α} :
list.of_fn f = list.pmap (λ (i : ) (hi : i < n), f i, hi⟩) (list.range n) _

theorem list.of_fn_eq_map {α : Type u_1} {n : } {f : fin n → α} :

theorem list.nodup_of_fn {α : Type u_1} {n : } {f : fin n → α} :