conjTranspose_invOf — Mathlib

English

The inverse of the conjugate transpose equals the conjugate transpose of the inverse: (A^H)^{-1} = (A^{-1})^H.

Русский

Обратная сопряжённого транспонирования равна сопряжённому транспонированному обратному: (A^H)^{-1} = (A^{-1})^H.

LaTeX

$$$(A^{\mathsf{H}})^{-1} = (A^{-1})^{\mathsf{H}}$$$

Lean4

theorem conjTranspose_invOf [Invertible A] [Invertible Aᴴ] : (⅟A)ᴴ = ⅟(Aᴴ) :=
  star_invOf _

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