Theorems · Theorem · linear algebra

SameRay.exists_eq_smul

∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {v₁ v₂ : M},
  SameRay R v₁ v₂ → ∃ u a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • u ∧ v₂ = b • u

If vectors v₁ and v₂ are on the same ray, then they are nonnegative multiples of the same vector. Actually, this vector can be assumed to be v₁ + v₂, see SameRay.exists_eq_smul_add.

Defined in

Mathlib.LinearAlgebra.Ray

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModule