isSymm_transpose_mul_self

Mathlib.LinearAlgebra.Matrix.Symmetric

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

English

The matrix Aᵀ A is symmetric for any A.

Русский

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

LaTeX

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

Lean4

theorem isSymm_transpose_mul_self [Fintype n] [NonUnitalCommSemiring α] (A : Matrix n n α) : (Aᵀ * A).IsSymm :=
  transpose_mul _ _

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

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

Разделы

Аффилиация

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