det_eq_sign_charpoly_coeff — Mathlib

English

The determinant of a square matrix equals (-1)^{n} times the constant term of its characteristic polynomial.

Русский

Определитель квадратной матрицы равен (-1)^n умножить на константный член её характеристического полинома.

LaTeX

$$$$ \\det(M) = (-1)^{|n|} \\operatorname{charpoly}(M).coeff(0). $$$$

Lean4

theorem det_eq_sign_charpoly_coeff (M : Matrix n n R) : M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0 :=
  by
  rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]
  simp

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