instNeg

Mathlib.Topology.Algebra.Module.Multilinear.Basic

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

English

The negation operation defines a Neg instance on continuous multilinear maps: the negation of f is the map sending m to −f(m).

Русский

Отрицание задаёт инстанс Neg на непрерывных мультилinear отображениях: (-f)(m) = −f(m).

LaTeX

$$(-f)(m) = -f(m)$$

Lean4

instance : Neg (ContinuousMultilinearMap R M₁ M₂) :=
  ⟨fun f => { -f.toMultilinearMap with cont := f.cont.neg }⟩

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

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

Разделы

Аффилиация

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