Theorems · Definition · linear algebra

SameRay

(R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] → {M : Type u_2} → [inst_3 : AddCommMonoid M] → [Module R M] → M → M → Prop

Two vectors are in the same ray if either one of them is zero or some positive multiples of them are equal (in the typical case over a field, this means one of them is a nonnegative multiple of the other).

Defined in

Mathlib.LinearAlgebra.Ray

Cited by

149 results in Mathlib

Foundations

Depth 12 from the axioms, rests on 122 definitions · uses no axioms

Assumes

CommSemiringPartialOrderIsStrictOrderedRingAddCommMonoidModule