eq_rotation_self_iff — Mathlib

English

A vector is fixed by rotation only when the angle is zero or the vector is zero.

Русский

Вектор зафиксирован поворотом только если угол нулевой или вектор нулевой.

LaTeX

$$x = o.rotation\ θ\ x \iff x = 0 \lor θ = 0$$

Lean4

/-- A vector equals a rotation of that vector if and only if the vector or the angle is zero. -/
theorem eq_rotation_self_iff (x : V) (θ : Real.Angle) : x = o.rotation θ x ↔ x = 0 ∨ θ = 0 := by
  rw [← rotation_eq_self_iff, eq_comm]

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