English
The oriented angle is nonzero and not π if and only if {x,y} is a linearly independent pair.
Русский
Угол не равен нулю и не равен π тогда и только тогда, когда пары x,y линейно независимы.
LaTeX
$$$o.oangle x y \neq 0 \land o.oangle x y \neq \pi \iff \text{LinearIndependent}_{\mathbb{R}}(x,y)$$$
Lean4
/-- The oriented angle between two vectors is zero or `π` if and only if the first vector is zero
or the second is a multiple of the first. -/
theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} :
o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x :=
by
rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg]
refine ⟨fun h => ?_, fun h => ?_⟩
· rcases h with (h | ⟨-, -, h⟩)
· by_cases hx : x = 0; · simp [hx]
obtain ⟨r, -, rfl⟩ := h.exists_nonneg_left hx
exact Or.inr ⟨r, rfl⟩
· by_cases hx : x = 0; · simp [hx]
obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx
refine Or.inr ⟨-r, ?_⟩
simp [hy]
· rcases h with (rfl | ⟨r, rfl⟩); · simp
by_cases hx : x = 0; · simp [hx]
rcases lt_trichotomy r 0 with (hr | hr | hr)
· rw [← neg_smul]
exact Or.inr ⟨hx, smul_ne_zero hr.ne hx, SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩
· simp [hr]
· exact Or.inl (SameRay.sameRay_pos_smul_right x hr)
