English
Reindexing a matrix by an equivalence changes the inverse correspondingly: inv(reindex e1 e2 A) = reindex e2 e1 (A^{-1}).
Русский
Перестановка индексов матрицы по эквивалентности требует соответствующей перестановки обратной: inv(reindex e1 e2 A) = reindex e2 e1 (A^{-1}).
LaTeX
$$inv (reindex e1 e2 A) = reindex e2 e1 (A⁻¹)$$
Lean4
@[simp]
theorem inv_submatrix_equiv (A : Matrix m m α) (e₁ e₂ : n ≃ m) : (A.submatrix e₁ e₂)⁻¹ = A⁻¹.submatrix e₂ e₁ :=
by
by_cases h : IsUnit A
· cases h.nonempty_invertible
letI := submatrixEquivInvertible A e₁ e₂
rw [← invOf_eq_nonsing_inv, ← invOf_eq_nonsing_inv, invOf_submatrix_equiv_eq A]
· have := (isUnit_submatrix_equiv e₁ e₂).not.mpr h
simp_rw [nonsing_inv_eq_ringInverse, Ring.inverse_non_unit _ h, Ring.inverse_non_unit _ this, submatrix_zero,
Pi.zero_apply]
