[Merged by Bors] - feat(linear_algebra/matrix/charpoly/eigs): det and trace are product and sum of eigenvalues

[MohanadAhmed]

This adds two lemmas:

1. det_eq_prod_roots_charpoly: the determinant of a square matrix is the product of the characteristic polynomial roots of that matrix.
2. trace_eq_sum_roots_charpoly: the trace is similarly the sum of the characteristic polynomial roots.

These two lemmas are more commonly stated as trace is the sum of eigenvalues and determinant is the product of eigenvalues. Mathlib has already defined eigenvalues in linear_algebra.eigenspace as the roots of the minimal polynomial of a linear endomorphism. These do not have correct multiplicity and cannot be used in the theorems above. Hence we express these theorems in terms of the roots of the characteristic polynomial directly.

---

[eric-wieser]

Can you add a note to the module docstring explaining the link to eigenvalues?

[MohanadAhmed]

@eric-wieser
Why the need to open linear_map module.End?

[MohanadAhmed]

So I figured out I can get away with using (ring_hom.id R) in place of the "bundled ring homomorphism". I still have no idea what that one is or this one is!!

[MohanadAhmed]

I think the condition [is_alg_closed], although stronger, is probably easier to understand and use (and if picked up as an instance more transparent to users with humble knowledge of ring homomorphisms). In this last bunch of commits I suggest we have two versions.

• The plain named ones det_eq_prod_roots_charpoly and trace_eq_sum_roots_charpoly which attempt to pick up the is_alg_closed instances themselves.
• We also have det_eq_prod_roots_charpoly_of_splits and trace_eq_sum_roots_charpoly_of_splits for the brave souls that can prove (or assume) their polynomial splits.

[MohanadAhmed]

What do you think @eric-wieser and @Vierkantor ? I mean about having two versions.

[Vierkantor]

So I figured out I can get away with using (ring_hom.id R) in place of the "bundled ring homomorphism". I still have no idea what that one is or this one is!!

That's an issue with the documentation if there is no explanation what we mean by the jargon "bundled". Could you point me to where you read this?

Ideally, to do mathematics in Lean we would only encounter ring homomorphisms in their bundled form. So if you don't see "unbundled" anywhere, don't worry about the word "bundled". So ring_hom.id R is a perfectly fine example of a homomorphism you can use here.

What we mean by "bundled" in mathlib is that objects carry proofs with them. So an element of R →+* S doesn't only contain the data of the map R → S but also the proofs showing that this map respects the ring structure.

[Vierkantor]

Thanks for the changes!

I tried to unify the commonalities with norm_gen_eq_prod_roots and trace_gen_eq_sum_roots myself, but had a few issues since prod_roots_eq_coeff_zero_of_monic_of_split is not quite general enough. So I propose that we merge this now with this TODO comment, and then come back to this later (after the mathlib4 port, probably). @eric-wieser, do you agree?

bors d+

[bors]

✌️ MohanadAhmed can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[MohanadAhmed]

v MohanadAhmed can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors r+

[bors]

Canceled.

[MohanadAhmed]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[eric-wieser]

Why does polynomial.splits take a morphism at all? Doesn't polynomial.splits_map_iff demonstrate that it's useless and we should just use (p.map f).splits instead?