angle_neg_neg

Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic

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

← MathLib Explorer

English

Let x and y be vectors. The angle between -x and -y is the same as the angle between x and y.

Русский

Пусть x и y — векторы. Угол между -x и -y равен углу между x и y.

LaTeX

$$$\\\\angle (-x) (-y) = \\\\angle x y$$$

Lean4

/-- The angle between the negation of two vectors. -/
@[simp]
theorem angle_neg_neg (x y : V) : angle (-x) (-y) = angle x y :=
  by
  unfold angle
  rw [inner_neg_neg, norm_neg, norm_neg]

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

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

Разделы

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

Аффилиация

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