Theorems · Theorem · geometry

Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul

∀ {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}, o.oangle x y = 0 ∨ o.oangle x y = ↑Real.pi ↔ x = 0 ∨ ∃ r, y = r • x

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.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact