English
For a pair of vectors, over a field, linear independence of {v_i, v_j} is equivalent to the only relation c v_i + d v_j = 0 being c = d = 0.
Русский
Для пары векторов над полем линейная независимость {v_i, v_j} эквивалентна тому, что единственное соотношение c v_i + d v_j = 0 имеет c = d = 0.
LaTeX
$$$\\mathrm{LinearIndepOn}_R( v, \\{i,j\\} ) \\iff \\forall c,d\\in R:\\ c\,v_i + d\,v_j = 0 \\Rightarrow c=0 \\land d=0$$$
Lean4
/-- `linearIndepOn_pair_iff` is a simpler version over fields. -/
theorem pair_iff {i j : ι} (f : ι → M) (hij : i ≠ j) :
LinearIndepOn R f { i, j } ↔ ∀ c d : R, c • f i + d • f j = 0 → c = 0 ∧ d = 0 := by
classical
rw [linearIndepOn_iff'']
refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩
· specialize h { i, j } (Pi.single i c + Pi.single j d)
simpa +contextual [Finset.sum_pair, Pi.single_apply, hij, hij.symm, hcd] using h
have ht' : t ⊆ { i, j } := by simpa [← Finset.coe_subset]
rw [Finset.sum_subset ht', Finset.sum_pair hij] at h0
· obtain ⟨hi0, hj0⟩ := h _ _ h0
exact fun k hkt ↦ Or.elim (ht hkt) (fun h ↦ h ▸ hi0) (fun h ↦ h ▸ hj0)
simp +contextual [hg0]
