det_permute — Mathlib

English

Permuting the columns 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_{\sigma,\mathrm{id}}) = \operatorname{sign}(\sigma) \det(M)$$$$

Lean4

/-- Permuting the columns changes the sign of the determinant. -/
theorem det_permute (σ : Perm n) (M : Matrix n n R) : (M.submatrix σ id).det = Perm.sign σ * M.det :=
  ((detRowAlternating : (n → R) [⋀^n]→ₗ[R] R).map_perm M σ).trans (by simp [Units.smul_def])

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