English
Let A be an n-by-n matrix over a commutative ring α. Consider the matrix X I_n + A, viewed as a matrix with polynomial entries in X over α. Then the determinant det(X I_n + A) is a monic polynomial in X; in particular, its leading coefficient is 1.
Русский
Пусть A — матрица размерности n×n над коммутативным кольцом α. Рассматривая det(X I_n + A) как многочлен по переменной X над α, получаем, что этот детерминант представляет собой монический многочлен, и его ведущий коэффициент равен 1.
LaTeX
$$$\operatorname{leadingCoeff}\bigl(\det(X I_n + A)\bigr) = 1$$$
Lean4
theorem leadingCoeff_det_X_one_add_C (A : Matrix n n α) :
leadingCoeff (det ((X : α[X]) • (1 : Matrix n n α[X]) + A.map C)) = 1 :=
by
cases subsingleton_or_nontrivial α
· simp [eq_iff_true_of_subsingleton]
rw [← @det_one n, ← coeff_det_X_add_C_card _ A, leadingCoeff]
simp only [Matrix.map_one, C_eq_zero, RingHom.map_one]
rcases (natDegree_det_X_add_C_le 1 A).eq_or_lt with h | h
· simp only [RingHom.map_one, Matrix.map_one, C_eq_zero] at h
rw [h]
· -- contradiction. we have a hypothesis that the degree is less than |n|
-- but we know that coeff _ n = 1
have H := coeff_eq_zero_of_natDegree_lt h
rw [coeff_det_X_add_C_card] at H
simp at H
