oangle_rotation_self_right

Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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

← MathLib Explorer

English

The angle between x and o.rotation θ x is θ: o.oangle(x, o.rotation θ x) = θ.

Русский

Угол между x и o.rotation θ x равен θ: o.oangle(x, o.rotation θ x) = θ.

LaTeX

$$$ o.oangle( x, o.rotation(\theta) x) = \theta $$$

Lean4

/-- A vector has an angle of `θ` from the rotation of that vector by `θ`. -/
theorem oangle_rotation_self_right {x : V} (hx : x ≠ 0) (θ : Real.Angle) : o.oangle x (o.rotation θ x) = θ := by
  simp [hx]

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

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

Разделы

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

Аффилиация

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