sameRay_neg_iff — Mathlib

English

If r < 0 and x and r•x lie on the same ray, then x = 0 (under NoZeroSmulDivisors).

Русский

Если r < 0 и x и r·x лежат на одном луче, то при условии NoZeroSmulDivisors выполняется x = 0.

LaTeX

$$$[NoZeroSMulDivisors\ R\ M] \; \text{hr} : r < 0 \land \mathrm{SameRay}(x, r\cdot x) \Rightarrow x = 0$$$

Lean4

/-- `SameRay.neg` as an `iff`. -/
@[simp]
theorem sameRay_neg_iff : SameRay R (-x) (-y) ↔ SameRay R x y := by simp only [SameRay, neg_eq_zero, smul_neg, neg_inj]

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