isUnit_submatrix_equiv — Mathlib

English

IsUnit of a submatrix equals IsUnit of the whole matrix under equivalence via submatrixEquivInvertibleEquivInvertible.

Русский

Единичность подматрицы равна единичности всей матрицы через эквивалентность.

LaTeX

$$IsUnit(A.submatrix e1 e2) ⇔ IsUnit(A)$$

Lean4

/-- When lowered to a prop, `Matrix.invertibleOfSubmatrixEquivInvertible` forms an `iff`. -/
@[simp]
theorem isUnit_submatrix_equiv {A : Matrix m m α} (e₁ e₂ : n ≃ m) : IsUnit (A.submatrix e₁ e₂) ↔ IsUnit A := by
  simp only [← nonempty_invertible_iff_isUnit, (submatrixEquivInvertibleEquivInvertible A _ _).nonempty_congr]

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