angle_neg_self_of_nonzero

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

URI: https://scilib.ai/kg/mathlib#InnerProductGeometry.angle_neg_self_of_nonzero

← MathLib Explorer

English

The angle between the negation of a nonzero vector and the vector equals π.

Русский

Угол между -x и x равен π для ненулевого x.

LaTeX

$$$\\\\angle (-x) x = \\\\pi$ при $x \\neq 0$$$

Lean4

/-- The angle between the negation of a nonzero vector and that
vector. -/
@[simp]
theorem angle_neg_self_of_nonzero {x : V} (hx : x ≠ 0) : angle (-x) x = π := by
  rw [angle_comm, angle_self_neg_of_nonzero hx]

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

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

Разделы

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

Аффилиация

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