instInvolutiveNeg

Mathlib.LinearAlgebra.Ray

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

← MathLib Explorer

English

Negating a ray and scaling by a unit is compatible: -u · v = -(u · v).

Русский

Отрицание луча и умножение единицей согласованы: -u · v = -(u · v).

LaTeX

$$$-u\cdot v = -(u\cdot v)$ for unit $u$.$$

Lean4

/-- Negating a nonzero vector twice produces the original vector. -/
instance {R : Type*} : InvolutiveNeg (RayVector R M)
    where
  neg := Neg.neg
  neg_neg v := by rw [Subtype.ext_iff, coe_neg, coe_neg, neg_neg]

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

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

Разделы

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

Аффилиация

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