det_submatrix_equiv_self — Mathlib

English

Permuting both indices of a matrix by the same equivalence e leaves the determinant unchanged: det(A.submatrix e e) = det(A).

Русский

Перестановка обеих индексов матрицы по одному и тому же эквиваленту e не меняет детерминант: det(A.submatrix e e) = det(A).

LaTeX

$$$$\det(A_{e,e}) = \det A$$$$

Lean4

/-- Permuting rows and columns with the same equivalence does not change the determinant. -/
@[simp]
theorem det_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m R) : det (A.submatrix e e) = det A :=
  by
  rw [det_apply', det_apply']
  apply Fintype.sum_equiv (Equiv.permCongr e)
  intro σ
  rw [Equiv.Perm.sign_permCongr e σ]
  congr 1
  apply Fintype.prod_equiv e
  intro i
  rw [Equiv.permCongr_apply, Equiv.symm_apply_apply, submatrix_apply]

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