English
Let h be a PowerBasis for a ring S over R. The characteristic polynomial of the linear map left multiplying by h.gen equals the minimal polynomial of h.gen: charpoly(leftMulMatrix h.basis h.gen) = minpoly R h.gen.
Русский
Пусть h — базис мощности для кольца S над R. Характеристический полином линейного отображения левого умножения на h.gen равен минимальному полиному h.gen: χ(leftMulMatrix(h.basis, h.gen)) = minpoly_R(h.gen).
LaTeX
$$$\\mathrm{charpoly}(\\mathrm{leftMulMatrix}(h.basis, h.gen)) = \\minpoly R h.gen$$$
Lean4
/-- The characteristic polynomial of the map `fun x => a * x` is the minimal polynomial of `a`.
In combination with `det_eq_sign_charpoly_coeff` or `trace_eq_neg_charpoly_coeff`
and a bit of rewriting, this will allow us to conclude the
field norm resp. trace of `x` is the product resp. sum of `x`'s conjugates.
-/
theorem charpoly_leftMulMatrix {S : Type*} [Ring S] [Algebra R S] (h : PowerBasis R S) :
(leftMulMatrix h.basis h.gen).charpoly = minpoly R h.gen :=
by
cases subsingleton_or_nontrivial R; · subsingleton
apply minpoly.unique' R h.gen (charpoly_monic _)
· apply (injective_iff_map_eq_zero (G := S) (leftMulMatrix _)).mp (leftMulMatrix_injective h.basis)
rw [← Polynomial.aeval_algHom_apply, aeval_self_charpoly]
refine fun q hq => or_iff_not_imp_left.2 fun h0 => ?_
rw [Matrix.charpoly_degree_eq_dim, Fintype.card_fin] at hq
contrapose! hq; exact h.dim_le_degree_of_root h0 hq
