oangle_rotation_left — Mathlib

English

The angle between o.rotation θ x and y satisfies o.oangle(o.rotation θ x, y) = o.oangle(x, y) − θ.

Русский

Угол между o.rotation θ x и y равен o.oangle(x, y) − θ.

LaTeX

$$$ o.oangle( o.rotation(\theta) x, y) = o.oangle(x, y) - \theta $$$

Lean4

/-- Rotating the first vector by `θ` subtracts `θ` from the angle between two vectors. -/
@[simp]
theorem oangle_rotation_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) :
    o.oangle (o.rotation θ x) y = o.oangle x y - θ :=
  by
  simp only [oangle, o.kahler_rotation_left']
  rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
  · abel
  · exact Circle.coe_ne_zero _
  · exact o.kahler_ne_zero hx hy

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