Theorems · Definition · linear algebra

Module.Ray.someRayVector

{R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Module.Ray R M → RayVector R M

An arbitrary RayVector giving a ray.

Defined in: Mathlib.LinearAlgebra.Ray
Cited by: 3 results in Mathlib
Foundations: Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring PartialOrder IsStrictOrderedRing AddCommMonoid Module

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
PartialOrderstatement and proof · cited by 6,410
IsStrictOrderedRingstatement and proof · cited by 2,490
Quotient.outproof · cited by 141
Module.Raystatement and proof · cited by 30
RayVectorstatement · cited by 7

Cited by4

Results whose statement or proof uses this declaration.

Module.Ray.someVectorproof · cited by 2
Module.Ray.someVector_ne_zeroproof · cited by 1
Module.Ray.someRayVector_raystatement · cited by 0
Module.Ray.someVector_rayproof · cited by 0