two_zsmul_oangle_neg_self_left

Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

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

← MathLib Explorer

English

Twice the angle between -x and x is 0: 2 · o.oangle(-x) x = 0.

Русский

Дважды угол между -x и x равен 0: 2 · o.oangle(-x) x = 0.

LaTeX

$$$2\,o.oangle(-x)\;x = 0$$$

Lean4

/-- Twice the angle between the negation of a vector and that vector is 0. -/
theorem two_zsmul_oangle_neg_self_left (x : V) : (2 : ℤ) • o.oangle (-x) x = 0 := by by_cases hx : x = 0 <;> simp [hx]

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

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

Разделы

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

Аффилиация

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