toFn_comp_ofFn_eq_id — Mathlib

English

For all n and v, toFn(n)(ofFn(n)(v)) = v; i.e., reconstructing the vector from its polynomial recovers the original vector.

Русский

Для всех n и v, toFn(n)(ofFn(n)(v)) = v; то есть восстановление вектора по многочлену дает исходный вектор.

LaTeX

$$$\operatorname{toFn}(n)(\operatorname{ofFn}(n)(v)) = v.$$$

Lean4

theorem toFn_comp_ofFn_eq_id (n : ℕ) (v : Fin n → R) : toFn n (ofFn n v) = v := by simp [toFn, ofFn, LinearMap.pi]

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