ofFn_coeff_eq_val_of_lt — Mathlib

English

The map ofFn(n): (Fin n → R) → R[X] is injective: different coefficient vectors give different polynomials.

Русский

Отображение ofFn(n) инъективно: разные векторы коэффициентов дают разные многочлены.

LaTeX

$$$\operatorname{Injective}(\operatorname{ofFn}(n)).$$$

Lean4

/-- If `i < n` the `i`-th coefficient of `ofFn n v` is `v i`. -/
@[simp]
theorem ofFn_coeff_eq_val_of_lt {n i : ℕ} (v : Fin n → R) (hi : i < n) : (ofFn n v).coeff i = v ⟨i, hi⟩ := by
  simp [ofFn, hi]

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