Partial unrolling of ∏ over a range?

Stream: new members

[Jake Kesinger]

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.

[Reid Barton]

See docs#finset.prod_range_succ

[Jake Kesinger]

oh and it was right there too. Thanks!

[Mario Carneiro]

#backticks

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

(deleted)