invertibleOfInvertibleConjTranspose

English

A matrix is invertible if its conjugate transpose is invertible; equivalently, invertibility transfers via conjugate transpose.

Русский

Матрица обратима тогда, когда её сопряжённое транспонированное обратимо; обратимость передаётся через сопряжённое транспонирование.

LaTeX

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

Lean4

/-- A matrix is invertible if the conjugate transpose is invertible. -/
def invertibleOfInvertibleConjTranspose [Invertible Aᴴ] : Invertible A :=
  by
  rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose]
  infer_instance

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