invertibleTranspose — Mathlib

English

If A is invertible, then A^T is invertible; in particular, the transpose preserves invertibility.

Русский

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

LaTeX

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

Lean4

/-- The transpose of an invertible matrix is invertible. -/
instance invertibleTranspose [Invertible A] : Invertible Aᵀ
    where
  invOf := (⅟A)ᵀ
  invOf_mul_self := by rw [← transpose_mul, mul_invOf_self, transpose_one]
  mul_invOf_self := by rw [← transpose_mul, invOf_mul_self, transpose_one]

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