From 0c44f3226511eec8ec0fbef477cc35921fe0fa2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= Date: Fri, 22 Nov 2024 11:41:25 +0000 Subject: [PATCH] docs(LinearAlgebra/Matrix/Determinant/Basic): det_submatrix_equiv_self (#19365) --- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean index 2571ccd9ad821..bd291498d65eb 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean @@ -209,7 +209,7 @@ theorem det_permute' (σ : Perm n) (M : Matrix n n R) : (M.submatrix id σ).det = Perm.sign σ * M.det := by rw [← det_transpose, transpose_submatrix, det_permute, det_transpose] -/-- Permuting rows and columns with the same equivalence has no effect. -/ +/-- 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