partialProd_succ — Mathlib

English

For f: Fin n → M and j: Fin n, the value of partialProd at j.succ equals partialProd at j.castSucc multiplied by f j.

Русский

Для f: Fin n → M и j: Fin n, partialProd(f, j.succ) = partialProd(f, j.castSucc) · f(j).

LaTeX

$$$$\\text{partialProd}(f, j.succ) = \\text{partialProd}(f, j.castSucc) \\cdot f(j).$$$$

Lean4

@[to_additive]
theorem partialProd_succ (f : Fin n → M) (j : Fin n) : partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
  simp [partialProd, List.take_succ]

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