English
If the family v is iIsOrtho with respect to B, and each v_i is not orthogonal to itself (i.e., B(v_i, v_i) ≠ 0), then the family {v_i} is linearly independent over the field K.
Русский
Если семейство v является iIsOrtho относительно B, и для каждого i вектор v_i не ортогонален самому себе (то есть B(v_i, v_i) ≠ 0), тогда множество {v_i} линейно независимо по полю K.
LaTeX
$$B.iIsOrtho v → (∀ i, ¬ B.IsOrtho (v i) (v i)) → LinearIndependent K v$$
Lean4
/-- A set of orthogonal vectors `v` with respect to some bilinear form `B` is linearly independent
if for all `i`, `B (v i) (v i) ≠ 0`. -/
theorem linearIndependent_of_iIsOrtho {n : Type w} {B : BilinForm K V} {v : n → V} (hv₁ : B.iIsOrtho v)
(hv₂ : ∀ i, ¬B.IsOrtho (v i) (v i)) : LinearIndependent K v := by
classical
rw [linearIndependent_iff']
intro s w hs i hi
have : B (s.sum fun i : n => w i • v i) (v i) = 0 := by rw [hs, zero_left]
have hsum : (s.sum fun j : n => w j * B (v j) (v i)) = w i * B (v i) (v i) :=
by
apply Finset.sum_eq_single_of_mem i hi
intro j _ hij
rw [iIsOrtho_def.1 hv₁ _ _ hij, mul_zero]
simp_rw [sum_left, smul_left, hsum] at this
exact eq_zero_of_ne_zero_of_mul_right_eq_zero (hv₂ i) this
