eq_zero_of_sum_eq_zero — Mathlib

English

Affine independence is preserved under affine equivalences.

Русский

Аффинная независимость сохраняется под аффинной эквивалентностью.

LaTeX

$$$\\forall p:\\; \\operatorname{AffineIndependent} k p \\iff \\operatorname{AffineIndependent} k (e\\circ p)$ for any $e:\\ P \\leftrightarrow P_2$ affine equivalence$$

Lean4

theorem eq_zero_of_sum_eq_zero (hp : AffineIndependent k p) (hw₀ : ∑ i ∈ s, w i = 0) (hw₁ : ∑ i ∈ s, w i • p i = 0) :
    ∀ i ∈ s, w i = 0 :=
  affineIndependent_iff.1 hp _ _ hw₀ hw₁

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