mul_invOf_cancel_right — Mathlib

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]

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