Theorems · Theorem · linear algebra

SameRay.exists_eq_smul_add

∀ {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₂ → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ v₁ = a • (v₁ + v₂) ∧ v₂ = b • (v₁ + v₂)

If vectors v₁ and v₂ are on the same ray, then for some nonnegative a b, a + b = 1, we have v₁ = a • (v₁ + v₂) and v₂ = b • (v₁ + v₂).

Defined in

Mathlib.LinearAlgebra.Ray

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRingAddCommGroupModule