submatrixEquivInvertible — Mathlib

English

Conjugating a matrix N by a unit M preserves its determinant: det(M N M^{-1}) = det N.

Русский

Сопряжение матрицы N единичной M сохраняет детерминант: det(M N M^{-1}) = det N.

LaTeX

$$det (M * N * M⁻¹) = det N$$

Lean4

/-- `A.submatrix e₁ e₂` is invertible if `A` is -/
def submatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible A] : Invertible (A.submatrix e₁ e₂) :=
  invertibleOfRightInverse _ ((⅟A).submatrix e₂ e₁) <| by
    rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]

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