R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
⊢ x = 0
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
⊢ x = 0
nontriviality M
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
⊢ x = 0
haveI : Nontrivial R := Module.nontrivial R M
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ x = 0
refine' eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) _
no goals
R : Type u_1
inst✝⁵ : StrictOrderedCommRing R
M : Type u_2
N : Type ?u.156166
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
x y : M
inst✝ : NoZeroSMulDivisors R M
h : SameRay R x (-x)
✝ : Nontrivial M
this : Nontrivial R
⊢ SameRay R x (-1 • x)
rwa [neg_one_smul]