eq_zero_of_forall_index_sum_pow_mul_eq_zero

English

Let f be an injective map from Fin n to a ring R and v : Fin n → R. If for every j in Fin n the sum ∑ i f(j)^i · v(i) equals 0, then v is identically zero.

Русский

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

LaTeX

$$$ \\forall j : Fin n, \\sum_{i : Fin n} f(j)^i \\cdot v(i) = 0 \\quad\\Rightarrow\\quad v = 0.$$$

Lean4

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

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