left_ne_zero_of_oangle_sign_eq_one

English

If the sign of the angle equals 1, then the first vector is nonzero.

Русский

Если знак угла равен 1, первый вектор ненулевой.

LaTeX

$$(o.oangle x y).sign = 1 ⇒ x ≠ 0$$

Lean4

/-- If the sign of the angle between two vectors is positive, the first vector is nonzero. -/
theorem left_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ 0 :=
  o.left_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0)

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