eq_zero_of_smul_mem_span — Mathlib

English

If a scalar multiple a v_i lies in the span of the other vectors {v_j : j ≠ i}, then a must be zero, given linear independence.

Русский

Если скалярное умножение a на v_i лежит во вдоль span остальных векторов {v_j : j ≠ i}, то a=0 при условии линейной независимости.

LaTeX

$$$a\,v_i \in \operatorname{span}(v''(univ \ {i})) \Rightarrow a=0$$$

Lean4

theorem eq_zero_of_smul_mem_span (hv : LinearIndependent R v) (i : ι) (a : R)
    (ha : a • v i ∈ span R (v '' (univ \ { i }))) : a = 0 :=
  by
  rw [Finsupp.span_image_eq_map_linearCombination, mem_map] at ha
  rcases ha with ⟨l, hl, e⟩
  rw [linearIndependent_iffₛ.1 hv l (Finsupp.single i a) (by simp [e])] at hl
  by_contra hn
  exact (notMem_of_mem_diff (hl <| by simp [hn])) (mem_singleton _)

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