mapMatrix_neg

Mathlib.Data.Matrix.Basic

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.mapMatrix_neg

English

The mapMatrix of a negation corresponds to negation of mapMatrix: (-f).mapMatrix = -(f.mapMatrix).

Русский

mapMatrix отрицания соответствует отрицанию mapMatrix: (-f).mapMatrix = -(f.mapMatrix).

LaTeX

$$$(-f).mapMatrix = -(f.mapMatrix)$$$

Lean4

@[simp]
theorem mapMatrix_neg [AddZeroClass α] [AddCommGroup β] (f : α →+ β) :
    (-f).mapMatrix = (-f.mapMatrix : Matrix m n α →+ _) :=
  rfl

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

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

Разделы

Аффилиация

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