rotation_eq_self_iff_angle_eq_zero

English

If x is nonzero, then rotating x by θ fixes x if and only if θ = 0.

Русский

Если x ≠ 0, тогда поворот x на угол θ фиксирует x тогда и только тогда, когда θ = 0.

LaTeX

$$(x ≠ 0) → (o.rotation\ θ\ x = x \iff θ = 0)$$

Lean4

/-- A rotation of a nonzero vector equals that vector if and only if the angle is zero. -/
@[simp]
theorem rotation_eq_self_iff_angle_eq_zero {x : V} (hx : x ≠ 0) (θ : Real.Angle) : o.rotation θ x = x ↔ θ = 0 :=
  by
  constructor
  · intro h
    rw [eq_comm]
    simpa [hx, h] using o.oangle_rotation_right hx hx θ
  · intro h
    simp [h]

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