neg

Mathlib.LinearAlgebra.Matrix.Symmetric

URI: https://scilib.ai/kg/mathlib#Matrix.IsSymm.neg

English

If A is symmetric, then -A is symmetric.

Русский

Если A симметрична, то -A симметрична.

LaTeX

$$$ \text{IsSymm}(A) \Rightarrow \text{IsSymm}(-A) $$$

Lean4

@[simp]
theorem neg [Neg α] {A : Matrix n n α} (h : A.IsSymm) : (-A).IsSymm :=
  (transpose_neg _).trans (congr_arg _ h)

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

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

Разделы

Аффилиация

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