oangle_rotation_oangle_left — Mathlib

English

The angle o.oangle( o.rotation( o.oangle x y) x, y) equals 0; i.e., rotating by the angle between x and y makes the pair orthogonal in Kahler sense.

Русский

Угол o.oangle( o.rotation( o.oangle x y) x, y) равен нулю; поворот на угол o.oangle x y делает пару ортогональной в Kahler-смысле.

LaTeX

$$$ o.oangle( o.rotation( o.oangle(x,y) ) x, y) = 0 $$$

Lean4

/-- Rotating the first vector by the angle between the two vectors results in an angle of 0. -/
@[simp]
theorem oangle_rotation_oangle_left (x y : V) : o.oangle (o.rotation (o.oangle x y) x) y = 0 :=
  by
  by_cases hx : x = 0
  · simp [hx]
  · by_cases hy : y = 0
    · simp [hy]
    · simp [hx, hy]

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