instNeg

Mathlib.LinearAlgebra.LinearPMap

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

English

The negation of a LinearPMap f is the LinearPMap with the same domain and the negated values.

Русский

Отрицание LinearPMap f имеет ту же область определения и значения равны сneg[f(x)].

LaTeX

$$$\mathrm{instNeg}.neg f$ имеет ту же домен и $ (\,-f) x = - f x$$$

Lean4

instance instNeg : Neg (E →ₗ.[R] F) :=
  ⟨fun f => ⟨f.domain, -f.toFun⟩⟩

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

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

Разделы

Аффилиация

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