Theorems · Theorem · linear algebra

Function.Injective.sameRay_map_iff

∀ {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] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {x y : M} {F : Type u_6} [inst_7 : FunLike F M N] [LinearMapClass F R M N] {f : F},
  Function.Injective ⇑f → (SameRay R (f x) (f y) ↔ SameRay R x y)

The images of two vectors under an injective linear map are on the same ray if and only if the original vectors are on the same ray.

Defined in

Mathlib.LinearAlgebra.Ray

Cited by

3 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringPartialOrderIsStrictOrderedRingAddCommMonoidModuleAddCommMonoidModuleFunLikeLinearMapClass