rotation_oangle_eq_iff_norm_eq — Mathlib

English

Rotating by the angle between x and y yields y if and only if the norms of x and y are equal.

Русский

Поворот на угол o.oangle x y x приводит к y тогда, когда нормы x и y равны.

LaTeX

$$o.rotation (o.oangle x y) x = y \iff ‖x‖ = ‖y‖$$

Lean4

/-- Rotating a vector by the angle to another vector gives the second vector if and only if the
norms are equal. -/
@[simp]
theorem rotation_oangle_eq_iff_norm_eq (x y : V) : o.rotation (o.oangle x y) x = y ↔ ‖x‖ = ‖y‖ :=
  by
  constructor
  · intro h
    rw [← h, LinearIsometryEquiv.norm_map]
  · intro h
    rw [o.eq_iff_oangle_eq_zero_of_norm_eq] <;> simp [h]

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