eq_zero_of_sameRay_neg_smul_right

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₁

Похожие утверждения