instDecidableIsSymmOfEqTranspose

Mathlib.LinearAlgebra.Matrix.Symmetric

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

English

If A is symmetric, then taking its transpose yields the same matrix: Aᵀ = A.

Русский

Если матрица A симметрична, то её транспонирование даёт ту же матрицу: Aᵀ = A.

LaTeX

$$$ \text{IsSymm}(A) \Rightarrow A^{\top} = A $$$

Lean4

instance (A : Matrix n n α) [Decidable (Aᵀ = A)] : Decidable (IsSymm A) :=
  inferInstanceAs <| Decidable (_ = _)

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

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

Разделы

Аффилиация

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