transpose

Mathlib.LinearAlgebra.Matrix.Hermitian

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

← MathLib Explorer

English

If A is Hermitian, then its transpose is Hermitian as well.

Русский

Если A эрмитова, то её транспонированная матрица тоже эрмитова.

LaTeX

$$$A^{\mathsf{T}}.IsHermitian$ given $A.IsHermitian$$$

Lean4

theorem transpose {A : Matrix n n α} (h : A.IsHermitian) : Aᵀ.IsHermitian :=
  by
  rw [IsHermitian, conjTranspose, transpose_map]
  exact congr_arg Matrix.transpose h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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