neg_of

Mathlib.LinearAlgebra.Matrix.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.neg_of

English

The embedding commutes with negation: negating the embedded function equals the embedding of the negated function.

Русский

Встраивание коммутирует с отрицанием: отрицание вложенной функции равно вложению отрицательной функции.

LaTeX

$$$ -\\mathrm{of}(f) = \\mathrm{of}(-f) $$$

Lean4

@[simp]
theorem neg_of [Neg α] (f : m → n → α) : -of f = of (-f) :=
  rfl

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

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

Разделы

Аффилиация

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