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]