Theorems · Theorem · geometry

Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero

∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(Real.pi / 2) ∨ o.oangle x y = ↑(-Real.pi / 2) ↔ inner ℝ x y = 0

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.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

3 results in Mathlib

Foundations

Depth 282 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact