map_succ — Mathlib

English

For a function a : Fin(n+1) → ℕ, map(d)(a) equals a(0) plus map(d) applied to a∘Fin.succ, times d: map(d)(a) = a(0) + map(d)(a ∘ Fin.succ) · d.

Русский

Для функции a: Fin(n+1) → ℕ верно: map(d)(a) = a(0) + map(d)(a ∘ Fin.succ) · d.

LaTeX

$$$ map(d)(a) = a(0) + map(d)(a \\circ Fin.succ) \\cdot d $$$

Lean4

theorem map_succ (a : Fin (n + 1) → ℕ) : map d a = a 0 + (∑ x : Fin n, a x.succ * d ^ (x : ℕ)) * d := by
  simp [map, Fin.sum_univ_succ, _root_.pow_succ, ← mul_assoc, ← sum_mul]

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