charpoly_leftMulMatrix

theorem charpoly_leftMulMatrix : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : Ring S] [inst_2 : Algebra R S] (h : PowerBasis R S), ((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

This theorem states that for any given power basis of an algebra over a commutative ring, the characteristic polynomial of the map `fun x => a * x` is equal to the minimal polynomial of `a`. This result is particularly useful in conjunction with other theorems such as `det_eq_sign_charpoly_coeff` or `trace_eq_neg_charpoly_coeff`, as it allows us to determine the field norm or trace of `x` as the product or sum, respectively, of `x`'s conjugates, with some rewriting.

More concisely: The characteristic polynomial of the multiplication-by-an-element map in a commutative algebra equals the minimal polynomial.