linearIndependent_unique_iff — Mathlib

English

If the index type is unique, linear independence is equivalent to nonzero value at the unique index.

Русский

Если индекс единственный, линейная независимость эквивалентна не нулю значению на единственном индексе.

LaTeX

$$$[\\text{Unique } ι] \\; \\text{LinearIndependent } R v \\iff v default \\neq 0$$$

Lean4

theorem linearIndependent_unique_iff (v : ι → M) [Unique ι] : LinearIndependent R v ↔ v default ≠ 0 :=
  by
  simp only [linearIndependent_iff, Finsupp.linearCombination_unique, smul_eq_zero]
  refine ⟨fun h hv => ?_, fun hv l hl => Finsupp.unique_ext <| hl.resolve_right hv⟩
  have := h (Finsupp.single default 1) (Or.inr hv)
  exact one_ne_zero (Finsupp.single_eq_zero.1 this)

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