invertibleOfSubmatrixEquivInvertible

English

There is an equivalence between invertible A and invertible A.submatrix e1 e2, realized by submatrixEquivInvertible and invertibleOfSubmatrixEquivInvertible.

Русский

Существует эквивалентность между обратимой A и обратимой A.submatrix e1 e2, реализуемая через submatrixEquivInvertible и invertibleOfSubmatrixEquivInvertible.

LaTeX

$$Invertible(A) ≃ Invertible(A.submatrix e1 e2)$$

Lean4

/-- `A` is invertible if `A.submatrix e₁ e₂` is -/
def invertibleOfSubmatrixEquivInvertible (A : Matrix m m α) (e₁ e₂ : n ≃ m) [Invertible (A.submatrix e₁ e₂)] :
    Invertible A :=
  invertibleOfRightInverse _ ((⅟(A.submatrix e₁ e₂)).submatrix e₂.symm e₁.symm) <|
    by
    have : A = (A.submatrix e₁ e₂).submatrix e₁.symm e₂.symm := by simp
    conv in _ * _ =>
      congr
      rw [this]
    rw [Matrix.submatrix_mul_equiv, mul_invOf_self, submatrix_one_equiv]

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