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

@[simp]
theorem det_pow (M : Matrix m m R) (n : ℕ) : det (M ^ n) = det M ^ n :=
  (detMonoidHom : Matrix m m R →* R).map_pow M n

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