invertibleOfInvertibleTranspose — Mathlib

English

If the conjugate transpose A^{T} is invertible, then A is invertible.

Русский

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

LaTeX

$$$\text{Invertible}(A^{T}) \Rightarrow \text{Invertible}(A)$$$

Lean4

/-- `Aᵀ` is invertible when `A` is. -/
def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A
    where
  invOf := (⅟(Aᵀ))ᵀ
  invOf_mul_self := by rw [← transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose]
  mul_invOf_self := by rw [← transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose]

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