feat: trace-nilpotency criterion

[jano-wol]

Trace-nilpotency criterion

This PR proves that over an algebraically closed field of characteristic zero, given subspaces A ≤ B of Module.End K V and the set M A B = {x | ∀ b ∈ B, ⁅x, b⁆ ∈ A}, any x ∈ M A B satisfying tr (x * y) = 0 for all y ∈ M A B is nilpotent.

Cartan's criterion proof overview following Humphreys, Ch. 4, pp. 31–32. We plan to deliver the proof in 3 steps:

1. This PR: Prove the trace-nilpotency criterion over algebraically closed fields. Uses Jordan–Chevalley decomposition, Lagrange interpolation.

2. Remove the algebraic closure assumption by scalar extension.

3. Prove Cartan's criterion by Engel's theorem + PR 2. This is the easiest out of the three steps.

[github-actions]

PR summary 7d9358ee9d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Lie.AdjointAction.JordanChevalley (new file)	1759
Mathlib.Algebra.Lie.NilpotentOfTrace (new file)	1812

---

Declarations diff

+ M
+ Module.End.aeval_apply_of_mem_eigenspace
+ Module.End.eval_zero_of_aeval_apply_eq_zero
+ ad_diag_basis
+ ad_mem_adjoin_of_isNilpotent
+ ad_mem_adjoin_of_isSemisimple
+ eval_zero_of_aeval_ad_eq
+ exists_polynomial_eval_sub
+ isNilpotent_of_trace_orthogonal_algClosed

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).