Algebra trace equals sum of roots of charpoly

Stream: Is there code for X?

[Alex Braat]

Is there a theorem like ring_theory.trace.trace_eq_sum_roots that does not assume that the algebra is a field?
Or some theorem that proves that the trace of a linear endomorphism of a finite dimensional vector space equals the sum of the roots of its characteristic polynomial?

[Anne Baanen]

For the linear map, you might get what you want by using docs#linear_map.to_matrix and then applying docs#matrix.trace_eq_neg_charpoly_coeff

[Anne Baanen]

For the connection of that coefficient with the roots we have docs#polynomial.sum_roots_eq_next_coeff_of_monic_of_split

[Anne Baanen]

I recall I stated the result for algebra traces for fields in order to make the minimal polynomial well-defined. We can probably extend it to any suitable pair S / R where minimal polynomials are unique but I'm not sure how well it would generalize beyond that.

[Alex Braat]

Thanks for the suggestions!

[Kevin Buzzard]

For min polys to be unique you need the ideal of $R[X]$ which annihiliates the endomorphism to be principal, and if $R$ isn't a field then $R[X]$ is very rarely a PID.

[Daan van Gent]

I agree that R should be a field, but there is not reason S should be a field, right? It suffices that R is a field and S is an R-algebra that is finitely generated as R-module.