English
If the index n has cardinality 2, then the characteristic polynomial of M is X^2 − (trace M) X + det M.
Русский
Если размерность n равна двум, то характеристический полином M имеет вид X^2 − tr(M) X + det(M).
LaTeX
$$$$ \\operatorname{charpoly}(M) = X^{2} - \\operatorname{tr}(M) X + \\operatorname{det}(M). $$$$
Lean4
theorem charpoly_of_card_eq_two [Nontrivial R] (hn : Fintype.card n = 2) :
M.charpoly = X ^ 2 - C M.trace * X + C M.det :=
by
have : Nonempty n := by rw [← Fintype.card_pos_iff]; omega
ext i
by_cases hi : i ∈ Finset.range 3
· fin_cases hi
· simp [det_eq_sign_charpoly_coeff, hn]
· simp [trace_eq_neg_charpoly_coeff, hn]
· simpa [leadingCoeff, charpoly_natDegree_eq_dim, hn, coeff_X] using M.charpoly_monic.leadingCoeff
· rw [Finset.mem_range, not_lt, Nat.succ_le] at hi
suffices M.charpoly.coeff i = 0 by
simpa [show i ≠ 2 by cutsat, show 1 ≠ i by cutsat, show i ≠ 0 by cutsat, coeff_X, coeff_C]
apply coeff_eq_zero_of_natDegree_lt
simpa [charpoly_natDegree_eq_dim, hn] using hi
