prod_take_succ — Mathlib

English

For any list L and index i, the product of the first i+1 elements equals the product of the first i elements times the i-th element: (L.take (i+1)).prod = (L.take i).prod · L[i].

Русский

Для списка L и индекса i произведение первых i+1 элементов равно произведению первых i элементов, умноженному на i-й элемент: (L.take (i+1)).prod = (L.take i).prod · L[i].

LaTeX

$$$ (L.take (i+1)).prod = (L.take i).prod \cdot L[i] $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_take_succ (L : List M) (i : ℕ) (p : i < L.length) : (L.take (i + 1)).prod = (L.take i).prod * L[i] :=
  by
  rw [← take_concat_get' _ _ p, prod_append]
  simp

Похожие утверждения