invOf_mul_cancel_right — Mathlib

English

(A^(-1))^H = (A^H)^(-1); i.e., the inverse commutes with conjugate transpose.

Русский

Обратная матрица в сопряженном транспонированном виде удовлетворяет (A^{-1})^H = (A^H)^{-1}.

LaTeX

$$$(A^{-1})^{\!H} = (A^{H})^{-1}$$$

Lean4

/-- A copy of `invOf_mul_cancel_right` for rectangular matrices. -/
protected theorem invOf_mul_cancel_right (A : Matrix m n α) (B : Matrix n n α) [Invertible B] : A * ⅟B * B = A := by
  rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]

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