English
A variant of the previous result, expressing the full product by pulling off the first term: ∏_{k=0}^{n} f(k) = f(0) · ∏_{i=0}^{n-1} f(i+1).
Русский
Вариант предшествующего вывода, который извлекает первый множитель: ∏_{k=0}^{n} f(k) = f(0) · ∏_{i=0}^{n-1} f(i+1).
LaTeX
$$$ ((\mathrm{range} n.succ).map f).prod = f(0) \cdot ((\mathrm{range} n).map (fun i \mapsto f i.succ)).prod $$$
Lean4
/-- A variant of `prod_range_succ` which pulls off the first term in the product rather than the
last. -/
@[to_additive /-- A variant of `sum_range_succ` which pulls off the first term in the sum rather
than the last. -/
]
theorem prod_range_succ' (f : ℕ → M) (n : ℕ) :
((range n.succ).map f).prod = f 0 * ((range n).map fun i ↦ f i.succ).prod :=
by
rw [range_succ_eq_map]
simp [Function.comp_def]
