ne_neg_self — Mathlib

English

A ray does not equal its own negation: x ≠ -x for any nonzero ray x.

Русский

Луч не равен своему собственному отрицанию: x ≠ -x для любого ненулевого луча x.

LaTeX

$$$x \neq -x$ for all $x$ in Module.Ray(R,M).$$$

Lean4

/-- A ray does not equal its own negation. -/
theorem ne_neg_self [NoZeroSMulDivisors R M] (x : Module.Ray R M) : x ≠ -x := by
  induction x using Module.Ray.ind with
  | h x hx =>
    rw [neg_rayOfNeZero, Ne, ray_eq_iff]
    exact mt eq_zero_of_sameRay_self_neg hx

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