det_mul_column — 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

/-- Multiplying each column by a fixed `v j` multiplies the determinant by
the product of the `v`s. -/
theorem det_mul_column (v : n → R) (A : Matrix n n R) : det (of fun i j => v i * A i j) = (∏ i, v i) * det A :=
  MultilinearMap.map_smul_univ _ v A

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