theorem
list.map_add_range'
(a s n : ℕ) :
list.map (has_add.add a) (list.range' s n) = list.range' (a + s) n
theorem
list.map_sub_range'
(a s n : ℕ) :
a ≤ s → list.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)
@[simp]
theorem
list.range'_append
(s m n : ℕ) :
list.range' s m ++ list.range' (s + m) n = list.range' s (n + m)
theorem
list.range_core_range'
(s n : ℕ) :
list.range_core s (list.range' s n) = list.range' 0 (n + s)
theorem
list.range_succ_eq_map
(n : ℕ) :
list.range (n + 1) = 0 :: list.map nat.succ (list.range n)
theorem
list.range'_eq_map_range
(s n : ℕ) :
list.range' s n = list.map (has_add.add s) (list.range n)
theorem
list.reverse_range'
(s n : ℕ) :
(list.range' s n).reverse = list.map (λ (i : ℕ), s + n - 1 - i) (list.range n)
All elements of fin n, from 0 to n-1.
Equations
- list.fin_range n = list.pmap fin.mk (list.range n) _
theorem
list.sum_range_succ
{α : Type u}
[add_monoid α]
(f : ℕ → α)
(n : ℕ) :
(list.map f (list.range n.succ)).sum = (list.map f (list.range n)).sum + f n
theorem
list.prod_range_succ
{α : Type u}
[monoid α]
(f : ℕ → α)
(n : ℕ) :
(list.map f (list.range n.succ)).prod = (list.map f (list.range n)).prod * f n
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 α) :
list.map prod.fst (list.enum_from n l) = list.range' n l.length
@[simp]
@[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.nodup_of_fn
{α : Type u_1}
{n : ℕ}
{f : fin n → α} :
function.injective f → (list.of_fn f).nodup