Zulip Chat Archive

Stream: new members

Topic: Partial unrolling of ∏ over a range?


view this post on Zulip Jake Kesinger (Oct 18 2020 at 18:54):

I'd like to be able to use the fact that a ∏ over a range is the last thing times the prod of all the other things, something like :

@[simp] lemma prod_unroll {R:Type*} [comm_ring R] (hyp: n > 0) (n: ℕ) (f:R→ℕ→R) (x:R):
(∏ i in range(n), (f x i)) = (
(∏ i in range(n-1), (f x i))
* (f x (n-1)) )
:=
begin
sorry
end

but I'm stumped as to how to prove this.

view this post on Zulip Reid Barton (Oct 18 2020 at 19:05):

See docs#finset.prod_range_succ

view this post on Zulip Jake Kesinger (Oct 18 2020 at 19:07):

oh and it was right there too. Thanks!

view this post on Zulip Mario Carneiro (Oct 18 2020 at 19:37):

#backticks

view this post on Zulip Yakov Pechersky (Oct 18 2020 at 20:08):

(deleted)

view this post on Zulip Yakov Pechersky (Oct 18 2020 at 20:09):

(deleted)


Last updated: May 10 2021 at 17:39 UTC