neg_of

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

Negation commutes with ofMatrix: -ofMatrix f = ofMatrix (-f).

Русский

Умножение на -1 сохраняется через ofMatrix: -ofMatrix f = ofMatrix (-f).

LaTeX

$$$[Neg A] (f : Matrix m n A) : -ofMatrix f = ofMatrix (-f)$$$

Lean4

@[simp]
theorem neg_of [Neg A] (f : Matrix m n A) : -ofMatrix f = ofMatrix (-f) :=
  rfl

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

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

Разделы

Аффилиация

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