oangle_rotation_right — Mathlib

English

The angle satisfies o.oangle(x, o.rotation θ y) = o.oangle(x, y) + θ.

Русский

Угол удовлетворяет o.oangle(x, o.rotation θ y) = o.oangle(x, y) + θ.

LaTeX

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

Lean4

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

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