neg_rotation_neg_pi_div_two — Mathlib

English

Negating rotation by -π/2 is equivalent to rotation by π/2.

Русский

Отрицание вращения на -π/2 эквивалентно вращению на π/2.

LaTeX

$$$-o.rotation(-π/2) = o.rotation(π/2)$$$

Lean4

/-- Negating a rotation by -π / 2 is equivalent to rotation by π / 2. -/
@[simp]
theorem neg_rotation_neg_pi_div_two (x : V) : -o.rotation (-π / 2 : ℝ) x = o.rotation (π / 2 : ℝ) x := by
  rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]

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