conjTranspose_neg

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

English

Conjugate transpose respects additive inverses: the conjugate transpose of −M is the negative of the conjugate transpose of M.

Русский

Сопряжённое транспонирование сохраняет отрицание: (−M)^H = − M^H.

LaTeX

$$$ (-M)^H = - M^H $$$

Lean4

@[simp]
theorem conjTranspose_neg [AddGroup α] [StarAddMonoid α] (M : Matrix m n α) : (-M)ᴴ = -Mᴴ :=
  Matrix.ext <| by simp

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

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

Разделы

Аффилиация

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