English
For a linear map f on a finite free module over a commutative ring, det f equals (-1)^{finrank} times the constant term of its characteristic polynomial: det f = (-1)^{finrank} · (charpoly f).coeff 0.
Русский
Для отображения f на конечном свободном модуле над коммутативным кольцом детерминант равен (-1)^{finrank} умноженному на константный член характеристического многочлена: det f = (-1)^{finrank} · (charpoly f).coeff 0.
LaTeX
$$$\det f = (-1)^{\operatorname{finrank} R M} \cdot (f.charpoly).coeff 0.$$$
Lean4
theorem det_eq_sign_charpoly_coeff {R M} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M]
[Module.Finite R M] (f : M →ₗ[R] M) : LinearMap.det f = (-1) ^ Module.finrank R M * f.charpoly.coeff 0 :=
by
nontriviality R
rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff, ←
Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
