oangle_rotation_self_left — Mathlib

English

The angle between o.rotation θ x and x is −θ: o.oangle(o.rotation θ x, x) = −θ.

Русский

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

LaTeX

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

Lean4

/-- The rotation of a vector by `θ` has an angle of `-θ` from that vector. -/
theorem oangle_rotation_self_left {x : V} (hx : x ≠ 0) (θ : Real.Angle) : o.oangle (o.rotation θ x) x = -θ := by
  simp [hx]

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