English
The oriented angle is ±π/2 iff the inner product is zero (orthogonality).
Русский
Угол ориентированный равен ±π/2 тогда и только тогда, когда скалярное произведение равно нулю (ортогональность).
LaTeX
$$$ x \perp y \iff o.oangle x y = \frac{\pi}{2} \text{ or } o.oangle x y = -\frac{\pi}{2} $$$
Lean4
/-- One of two vectors is zero or the oriented angle between them is plus or minus `π / 2` if
and only if the inner product of those vectors is zero. -/
theorem eq_zero_or_oangle_eq_iff_inner_eq_zero {x y : V} :
x = 0 ∨ y = 0 ∨ o.oangle x y = (π / 2 : ℝ) ∨ o.oangle x y = (-π / 2 : ℝ) ↔ ⟪x, y⟫ = 0 :=
by
by_cases hx : x = 0; · simp [hx]
by_cases hy : y = 0; · simp [hy]
rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right hy]
refine ⟨fun h => ?_, fun h => ?_⟩
· rwa [o.angle_eq_abs_oangle_toReal hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff]
· convert o.oangle_eq_angle_or_eq_neg_angle hx hy using 2 <;> rw [h]
simp only [neg_div, Real.Angle.coe_neg]
