conjTranspose_transpose

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

English

The conjugate of the transpose equals the transpose of the conjugate: M^H^T = M^*.

Русский

Сопряжение после транспонирования равно транспонированию после сопряжения: M^{HT} = M^{*}.

LaTeX

$$$ M^{H T} = M^{*} $$$

Lean4

theorem conjTranspose_transpose [Star α] (M : Matrix m n α) : Mᴴᵀ = M.map star :=
  rfl

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

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

Разделы

Аффилиация

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