eq_zero_of_smul_mem_span — Mathlib

English

If a family {v_i} indexed by i in s is linearly independent in its restriction to s, then each v_i is not in the span of the others within s, i.e., no vector in the family is a linear combination of the rest contained in s.

Русский

Если семейство {v_i} на множeстве s линейно независимо, тогда каждый v_i не принадлежит span остальных элементов внутри s.

LaTeX

$$v_i ∉ span R (v '' (s \ { i }))$$

Lean4

nonrec theorem eq_zero_of_smul_mem_span (hv : LinearIndepOn R v s) (hi : i ∈ s) (a : R)
    (ha : a • v i ∈ span R (v '' (s \ { i }))) : a = 0 :=
  hv.eq_zero_of_smul_mem_span ⟨i, hi⟩ _ <| by simpa [← comp_def, image_comp, image_diff Subtype.val_injective]

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