partialProd_init — Mathlib

English

Let f: Fin(n+1) → M. For i ∈ Fin(n+1), partialProd( init f ) i equals partialProd f i.castSucc.

Русский

Пусть f: Fin(n+1) → M. Тогда partialProd( init f ) i = partialProd f( i.castSucc ).

LaTeX

$$$$\\text{partialProd}(\\text{init } f, i) = \\text{partialProd}(f, i^{\\mathrm{castSucc}}).$$$$

Lean4

@[to_additive]
theorem partialProd_init {f : Fin (n + 1) → M} (i : Fin (n + 1)) : partialProd (init f) i = partialProd f i.castSucc :=
  i.inductionOn (by simp) fun i hi => by simp_all [init, partialProd_succ]

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