Skip to content

Commit

Permalink
docs(LinearAlgebra/Matrix/Determinant/Basic): det_submatrix_equiv_self (
Browse files Browse the repository at this point in the history
  • Loading branch information
madvorak committed Nov 22, 2024
1 parent 81381ad commit 0c44f32
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 0c44f32

Please sign in to comment.