invertibleConjTranspose

Mathlib.Data.Matrix.Invertible

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

← MathLib Explorer

English

If A is invertible, then the conjugate transpose A^H is invertible as well.

Русский

Если A обратима, то обратимо и сопряженно-транспонированная матрица A^H.

LaTeX

$$$\text{Invertible}(A) \Rightarrow \text{Invertible}(A^{\mathsf{H}}).$$$

Lean4

/-- The conjugate transpose of an invertible matrix is invertible. -/
instance invertibleConjTranspose [Invertible A] : Invertible Aᴴ :=
  Invertible.star _

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

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

Разделы

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

Аффилиация

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