invOf_submatrix_equiv_eq — Mathlib

English

The inverse of a submatrix equals the corresponding submatrix of the inverse of A.

Русский

Обратная подматрица равна соответствующей подматрице обратной матрицы A.

LaTeX

$$⅟(A.submatrix e1 e2) = (⅟A).submatrix e2 e1$$

Lean4

theorem invOf_submatrix_equiv_eq (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] [Invertible (A.submatrix e₁ e₂)] :
    ⅟(A.submatrix e₁ e₂) = (⅟A).submatrix e₂ e₁ :=
  by
  rw [@Invertible.congr _ _ _ _ _ (submatrixEquivInvertible A e₁ e₂) rfl]
  rfl

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