neg_rotation_pi_div_two

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

URI: https://scilib.ai/kg/mathlib#Orientation.neg_rotation_pi_div_two

← MathLib Explorer

English

Negating a rotation by π/2 equals rotation by -π/2.

Русский

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

LaTeX

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

Lean4

/-- Negating a rotation by π / 2 is equivalent to rotation by -π / 2. -/
theorem neg_rotation_pi_div_two (x : V) : -o.rotation (π / 2 : ℝ) x = o.rotation (-π / 2 : ℝ) x :=
  (neg_eq_iff_eq_neg.mp <| o.neg_rotation_neg_pi_div_two _).symm

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru