Theorems · Theorem · geometry

Orientation.oangle_sign_smul_add_smul_right

∀ {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) (r₁ r₂ : ℝ),
  (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign

The sign of the angle between a vector, and a linear combination of that vector with a second vector, is the sign of the factor by which the second vector is multiplied in that combination multiplied by the sign of the angle between the two vectors.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact