oangle_rotation — Mathlib

English

Rotating both vectors by the same angle does not change the oriented angle between them.

Русский

Повернув оба вектора на одинаковый угол, ориентированный угол между ними не меняется.

LaTeX

$$$o.oangle (o.rotation\ θ\ x) (o.rotation\ θ\ y) = o.oangle x y$$$

Lean4

/-- Rotating both vectors by the same angle does not change the angle between those vectors. -/
@[simp]
theorem oangle_rotation (x y : V) (θ : Real.Angle) : o.oangle (o.rotation θ x) (o.rotation θ y) = o.oangle x y := by
  by_cases hx : x = 0 <;> by_cases hy : y = 0 <;> simp [hx, hy]

Похожие утверждения