English
The characteristic polynomial of a square matrix is monic (leading coefficient is 1).
Русский
Характеристический полином квадратной матрицы моничен (ведущий коэффициент равен 1).
LaTeX
$$$$ \\operatorname{charpoly}(M) \\text{ is monic}. $$$$
Lean4
theorem charpoly_monic (M : Matrix n n R) : M.charpoly.Monic :=
by
nontriviality R
by_cases h : Fintype.card n = 0
· rw [charpoly, det_eq_one_of_card_eq_zero h]
apply monic_one
have mon : (∏ i : n, (X - C (M i i))).Monic :=
by
apply monic_prod_of_monic univ fun i : n => X - C (M i i)
simp [monic_X_sub_C]
rw [← sub_add_cancel (∏ i : n, (X - C (M i i))) M.charpoly] at mon
rw [Monic] at *
rwa [leadingCoeff_add_of_degree_lt] at mon
rw [charpoly_degree_eq_dim]
rw [← neg_sub]
rw [degree_neg]
apply lt_trans (charpoly_sub_diagonal_degree_lt M)
rw [Nat.cast_lt]
cutsat
