eq_zero_of_forall_pow_sum_mul_pow_eq_zero

English

Let R be a domain and f : Fin n → R be injective. If v : Fin n → R satisfies ∑_j v_j f(j)^i = 0 for all i ∈ Fin n, then v = 0.

Русский

Пусть R — домен, f: Fin n → R инъективна. Если вектор v : Fin n → R удовлетворяет ∑_j v_j f(j)^i = 0 для всех i ∈ Fin n, то v = 0.

LaTeX

$$$[IsDomain\\ R] \\Rightarrow (\\text{If } f: \\mathrm{Fin}\\ n \\to R \\text{ is injective and } \\forall i:\\mathrm{Fin}\\ n, \\ \\sum_{j:\\mathrm{Fin}\\ n} v_j f(j)^i = 0) \\Rightarrow v = 0.$$$

Lean4

theorem eq_zero_of_forall_pow_sum_mul_pow_eq_zero [IsDomain R] {f v : Fin n → R} (hf : Function.Injective f)
    (hfv : ∀ i : Fin n, (∑ j : Fin n, v j * f j ^ (i : ℕ)) = 0) : v = 0 :=
  eq_zero_of_vecMul_eq_zero (det_vandermonde_ne_zero_iff.mpr hf) (funext hfv)

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