partialProd_succ' — Mathlib

English

For f: Fin(n+1) → M and j: Fin(n+1), partialProd(f, j.succ) equals f(0) times partialProd(Fin.tail f) evaluated at j.

Русский

Для f: Fin(n+1) → M и j: Fin(n+1), partialProd(f, j.succ) = f(0) · partialProd(Fin.tail f)(j).

LaTeX

$$$$\\text{partialProd}(f, j.succ) = f(0) \\cdot \\text{partialProd}(\\text{Fin.tail } f, j).$$$$

Lean4

@[to_additive]
theorem partialProd_succ' (f : Fin (n + 1) → M) (j : Fin (n + 1)) :
    partialProd f j.succ = f 0 * partialProd (Fin.tail f) j :=
  by
  simp [partialProd]
  rfl

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