vandermonde_succ — Mathlib

English

vandermonde v for a successor type equals the concatenation form Fin.cons with a base row and tail recursion.

Русский

Vandermonde для типа продолжения совпадает с конкатенацией Fin.cons на основе базовой строки и хвостовой рекурсии.

LaTeX

$$$\\mathrm{vandermonde}(v) = \\mathrm{projVandermonde}(v,1)$$$

Lean4

theorem vandermonde_succ (v : Fin n.succ → R) :
    vandermonde v =
      .of Fin.cons (fun (j : Fin n.succ) => v 0 ^ (j : ℕ)) fun i =>
        Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j :=
  by
  conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]
  rfl

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