eq_zero_of_sameRay_self_neg — Mathlib

English

If a vector is in the same ray as its own negation, then the vector is zero (under NoZeroSmulDivisors).

Русский

Если вектор лежит на том же луче, что и его собственное отрицание, то вектор равен нулю (при NoZeroSmulDivisors).

LaTeX

$$$x = 0$ if $\mathrm{SameRay}(x, -x)$ (NoZeroSmulDivisors).$$$

Lean4

/-- If a vector is in the same ray as its negation, that vector is zero. -/
theorem eq_zero_of_sameRay_self_neg [NoZeroSMulDivisors R M] (h : SameRay R x (-x)) : x = 0 :=
  by
  nontriviality M; haveI : Nontrivial R := Module.nontrivial R M
  refine eq_zero_of_sameRay_neg_smul_right (neg_lt_zero.2 (zero_lt_one' R)) ?_
  rwa [neg_one_smul]

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