Theorems · Theorem · number theory

LinearMap.BilinForm.linearIndependent_of_pairwise_le_zero

∀ {ι : Type u_4} {R : Type u_5} {M : Type u_6} [inst : CommRing R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (B : LinearMap.BilinForm R M),
  (LinearMap.BilinMap.toQuadraticMap B).PosDef →
    ∀ (f : Module.Dual R M) (v : ι → M),
      (∀ (i : ι), 0 < f (v i)) → (Pairwise fun i j => (B (v i)) (v j) ≤ 0) → LinearIndependent R v

Vectors which subtend obtuse angles with each other and all lie in the same half-space are linearly independent. This is [serre1965](Ch. V, §9, Lemma 4).

Defined in

Mathlib.LinearAlgebra.QuadraticForm.Dual

Cited by

1 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLinearOrderIsStrictOrderedRingAddCommGroupModule