det_permute' — Mathlib

English

Permuting the rows by a permutation σ changes the determinant by the sign of σ: det(M.submatrix(id, σ)) = sign(σ) det(M).

Русский

Перестановка строк матрицы по перестановке σ изменяет детерминант на знак σ: det(M.submatrix(id, σ)) = sign(σ) det(M).

LaTeX

$$$$\det(M_{\mathrm{id},\sigma}) = \operatorname{sign}(\sigma) \det(M)$$$$

Lean4

/-- Permuting the rows changes the sign of the determinant. -/
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]

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