transpose

Mathlib.LinearAlgebra.Matrix.IsDiag

URI: https://scilib.ai/kg/mathlib#Matrix.IsDiag.transpose

English

If A is diagonal, then its transpose A^T is diagonal.

Русский

Если A диагональная, то A^T диагональна.

LaTeX

$$$\\forall {\\alpha} {A : Matrix n n \\alpha} (ha : A.IsDiag) : A^T.IsDiag$$$

Lean4

theorem transpose [Zero α] {A : Matrix n n α} (ha : A.IsDiag) : Aᵀ.IsDiag := fun _ _ h => ha h.symm

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

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

Разделы

Аффилиация

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