isSymm_transpose_add_self

Mathlib.LinearAlgebra.Matrix.Symmetric

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

English

The matrix Aᵀ + A is symmetric for any A (same as previous item).

Русский

Матрица Aᵀ + A симметрична для любой A.

LaTeX

$$$ (A^{\top} + A)^{\top} = A^{\top} + A $$$

Lean4

theorem isSymm_transpose_add_self [AddCommSemigroup α] (A : Matrix n n α) : (Aᵀ + A).IsSymm :=
  add_comm _ _

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

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

Разделы

Аффилиация

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