From 931f90e5533e974eabefda790858ad6dd2a12f8b Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Wed, 10 Jul 2019 11:57:51 -0400 Subject: [PATCH] feat(data/list/basic): list.prod_range_succ, list.sum_range_succ (#1197) * feat(data/list/basic): list.prod_range_succ, list.sum_range_succ * changes from review * remove simp * shorten proof --- src/data/list/basic.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/data/list/basic.lean b/src/data/list/basic.lean index a9dd2741cb8df..3f85347ef5aa3 100644 --- a/src/data/list/basic.lean +++ b/src/data/list/basic.lean @@ -4209,7 +4209,7 @@ mt mem_range.1 $ lt_irrefl _ theorem nth_range {m n : ℕ} (h : m < n) : nth (range n) m = some m := by simp only [range_eq_range', nth_range' _ h, zero_add] -theorem range_concat (n : ℕ) : range (n + 1) = range n ++ [n] := +theorem range_concat (n : ℕ) : range (succ n) = range n ++ [n] := by simp only [range_eq_range', range'_concat, zero_add] theorem iota_eq_reverse_range' : ∀ n : ℕ, iota n = reverse (range' 1 n) @@ -4250,6 +4250,12 @@ nodup_pmap (λ _ _ _ _, fin.veq_of_eq) (nodup_range _) @[simp] lemma length_fin_range (n : ℕ) : (fin_range n).length = n := by rw [fin_range, length_pmap, length_range] +@[to_additive list.sum_range_succ] +theorem prod_range_succ {α : Type u} [monoid α] (f : ℕ → α) (n : ℕ) : + ((range n.succ).map f).prod = ((range n).map f).prod * f n := +by rw [range_concat, map_append, map_singleton, + prod_append, prod_cons, prod_nil, mul_one] + /-- `Ico n m` is the list of natural numbers `n ≤ x < m`. (Ico stands for "interval, closed-open".)