Theorems · Theorem · geometry

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

The sign of the angle between two linear combinations of two vectors is the sign of the determinant of the factors in those combinations multiplied by the sign of the angle between the two vectors.

Defined in

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact