eq_rotation_self_iff_angle_eq_zero

English

A nonzero vector equals a rotation of itself if and only if the rotation angle is zero.

Русский

Не нулевой вектор равен своему повороту тогда и только тогда, когда угол поворота равен нулю.

LaTeX

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

Lean4

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

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