charpoly_fin_two — Mathlib

English

For any matrix M over a ring with two elements in Finite type, the characteristic polynomial takes the standard 2×2 form.

Русский

Для любой матрицы над кольцом в случае Finite 2 элементной размерности характерполином принимает стандартную форму 2×2.

LaTeX

$$$$ \\operatorname{charpoly}(M) = X^{2} - C(\\operatorname{tr} M) X + C(\\det M). $$$$

Lean4

theorem charpoly_fin_two [Nontrivial R] (M : Matrix (Fin 2) (Fin 2) R) : M.charpoly = X ^ 2 - C M.trace * X + C M.det :=
  M.charpoly_of_card_eq_two <| Fintype.card_fin _

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