isSymm_add_transpose_self

Mathlib.LinearAlgebra.Matrix.Symmetric

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

English

The matrix Aᵀ + A is symmetric for any A in a semiring with commutative addition.

Русский

Матрица Aᵀ + A симметрична для любой A в полюке с коммутативным сложением.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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