det_eq_prod_roots_charpoly — Mathlib

English

Over an algebraically closed field, det(A) equals the product of the roots of its characteristic polynomial: det(A) = (charpoly(A)).roots.prod.

Русский

В алгебраически замкнутом поле детерминант равен произведению корней характеристического полинома: det(A) = (charpoly(A)).roots.prod.

LaTeX

$$A.det = A.charpoly.roots.prod$$

Lean4

theorem det_eq_prod_roots_charpoly [IsAlgClosed K] : A.det = (Matrix.charpoly A).roots.prod :=
  det_eq_prod_roots_charpoly_of_splits (IsAlgClosed.splits A.charpoly)

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