neg

Mathlib.LinearAlgebra.TensorProduct.Basic

URI: https://scilib.ai/kg/mathlib#TensorProduct.neg

English

In the tensor product, negation cancels addition: -x + x = 0 for all x.

Русский

В тензорном произведении отрицание и сложение взаимоисключают друг друга: -x + x = 0.

LaTeX

$$$$-x + x = 0.$$$$

Lean4

instance neg : Neg (M ⊗[R] N) where neg := Neg.aux R

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

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

Разделы

Аффилиация

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