rotation_pi

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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

English

Rotation by π is the negation: o.rotation(π) = neg.

Русский

Поворот на π эквивалентен отрицанию: o.rotation(π) = neg.

LaTeX

$$$ o.rotation(\pi) = \mathrm{neg} \\quad$ (linear isometry negation)$$

Lean4

/-- Rotation by π is negation. -/
@[simp]
theorem rotation_pi : o.rotation π = LinearIsometryEquiv.neg ℝ :=
  by
  ext x
  simp [rotation]

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

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

Разделы

Аффилиация

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