neg_rotation

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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

← MathLib Explorer

English

Negating a rotation by θ is the same as rotating by π + θ.

Русский

Отрицание вращения на θ эквивалентно вращению на π + θ.

LaTeX

$$$-o.rotation\, θ\, x = o.rotation\,(π + θ)\, x$$$

Lean4

/-- Negating a rotation is equivalent to rotation by π plus the angle. -/
theorem neg_rotation (θ : Real.Angle) (x : V) : -o.rotation θ x = o.rotation (π + θ) x := by
  rw [← o.rotation_pi_apply, rotation_rotation]

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

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

Разделы

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

Аффилиация

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