rotation_pi_apply

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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

English

Rotation by π/2 equals the right-angle rotation J: o.rotation(π/2) = J.

Русский

Поворот на π/2 равен правоугольному повороту J: o.rotation(π/2) = J.

LaTeX

$$$ o.rotation(\tfrac{\pi}{2}) = J $$$

Lean4

/-- Rotation by π is negation. -/
theorem rotation_pi_apply (x : V) : o.rotation π x = -x := by simp

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

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

Разделы

Аффилиация

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