instNeg

Mathlib.LinearAlgebra.Ray

URI: https://scilib.ai/kg/mathlib#RayVector.instNeg

English

Negation on rays is involutive: neg(neg(v)) = v for all rays v.

Русский

Отрицание лучей инволютивно: двойное отрицание луча возвращает исходный луч.

LaTeX

$$$\text{neg}(\text{neg}(v)) = v$ for all $v \in \mathrm{Module.Ray}(R,M)$.$$

Lean4

/-- Negating a nonzero vector. -/
instance {R : Type*} : Neg (RayVector R M) :=
  ⟨fun v => ⟨-v, neg_ne_zero.2 v.prop⟩⟩

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

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

Разделы

Аффилиация

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