isSymm_one

Mathlib.LinearAlgebra.Matrix.Symmetric

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

English

The identity matrix is symmetric: Iᵀ = I.

Русский

Единичная матрица симметрична: Iᵀ = I.

LaTeX

$$$ I^{\top} = I $$$

Lean4

@[simp]
theorem isSymm_one [DecidableEq n] [Zero α] [One α] : (1 : Matrix n n α).IsSymm :=
  transpose_one

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

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

Разделы

Аффилиация

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