det_eq_prod_roots_charpoly_of_splits

English

If the characteristic polynomial splits over K, the determinant equals the product of its roots: det(A) = charpoly(A).roots.prod.

Русский

Если характеристический полином раскладывается над K, то детерминант равен произведению его корней: det(A) = charpoly(A).roots.prod.

LaTeX

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

Lean4

theorem det_eq_prod_roots_charpoly_of_splits (hAps : A.charpoly.Splits (RingHom.id K)) :
    A.det = (Matrix.charpoly A).roots.prod := by
  rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim A,
    Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits A.charpoly_monic hAps, ← mul_assoc, ← pow_two,
    pow_right_comm, neg_one_sq, one_pow, one_mul]

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