English
If for NoZeroSmulDivisors a ray is represented by a vector and its negation, certain negation identities hold; (alternate form).
Русский
Если для NoZeroSmulDivisors луч задаётся вектором и его негативом, выполняются идентичности отрицания; (альтернативная формулировка).
LaTeX
$$$\ldots$$$
Lean4
theorem eq_zero_of_sameRay_neg_smul_right [NoZeroSMulDivisors R M] {r : R} (hr : r < 0) (h : SameRay R x (r • x)) :
x = 0 := by
rcases h with (rfl | h₀ | ⟨r₁, r₂, hr₁, hr₂, h⟩)
· rfl
· simpa [hr.ne] using h₀
· rw [← sub_eq_zero, smul_smul, ← sub_smul, smul_eq_zero] at h
refine h.resolve_left (ne_of_gt <| sub_pos.2 ?_)
exact (mul_neg_of_pos_of_neg hr₂ hr).trans hr₁