English
The transpose of an invertible matrix is invertible; in particular, A^T is invertible if A is invertible.
Русский
Транспонированная матрица, являющаяся обратимой, обратима тогда, когда сама матрица обратно применима.
LaTeX
$$$\text{Invertible}(A) \implies \text{Invertible}(A^{T}).$$$
Lean4
/-- A copy of `mul_invOf_cancel_right` for rectangular matrices. -/
protected theorem mul_invOf_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * B * ⅟B = A := by
rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]