charpoly_coeff_eq_prod_coeff_of_le

English

If k is large enough (at least card(n) − 1), then the k-th coefficient of the characteristic polynomial equals the k-th coefficient of the product over diagonal entries (X − C(M_{ii})).

Русский

При k ≥ card(n)−1 коэффициент k характеристического полинома равен коэффициенту k произведения по диагонали матрицы: ∏ (X − C(M_{ii})).

LaTeX

$$$$ M^{\\text{charpoly}}_{k} = \\left( \\prod_{i \\in n} (X - C(M_{ii})) \\right)_{k}, \\quad \\text{если } card(n) - 1 \\le k. $$$$

Lean4

theorem charpoly_coeff_eq_prod_coeff_of_le {k : ℕ} (h : Fintype.card n - 1 ≤ k) :
    M.charpoly.coeff k = (∏ i : n, (X - C (M i i))).coeff k :=
  by
  apply eq_of_sub_eq_zero; rw [← coeff_sub]
  apply Polynomial.coeff_eq_zero_of_degree_lt
  apply lt_of_lt_of_le (charpoly_sub_diagonal_degree_lt M) ?_
  rw [Nat.cast_le]; apply h

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