[Merged by Bors] - feat(Analysis/InnerProductSpace): transfer lemmas about charpoly/eigenvalues from matrix to linear map

[wwylele]

These are some lemmas existing for matrix but missing for linear map.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

---

AI usage disclosure: I used Aristotle initially to one-shot the missing lemma LinearMap.det_eq_prod_eigenvalues, and then worked manually to break them into small pieces and align them with existing lemmas.

Here is a list of correspondence between new lemma and existing ones. Some of these have names and statements that I wouldn't be sure about if I had come up on my own, so I used the existing ones as justification for how they are named / stated

• LinearMap.IsSymmetric.charpoly_eq - Matrix.IsHermitian.charpoly_eq
• LinearMap.IsSymmetric.roots_charpoly_eq_eigenvalues - Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀
• LinearMap.IsSymmetric.sort_roots_charpoly_eq_eigenvalues - Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀
• LinearMap.IsSymmetric.eigenvalues_eq_eigenvalues_iff - Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff
• LinearMap.IsSymmetric.splits_charpoly - Matrix.IsHermitian.splits_charpoly
• LinearMap.IsSymmetric.det_eq_prod_eigenvalues - Matrix.IsHermitian.det_eq_prod_eigenvalues

[github-actions]

PR summary be85740951

Import changes exceeding 2%

%	File
+3.50%	Mathlib.LinearAlgebra.Eigenspace.Charpoly

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.Eigenspace.Charpoly	1684	1743	+59 (+3.50%)
Mathlib.Analysis.InnerProductSpace.Spectrum	2360	2369	+9 (+0.38%)
Mathlib.Analysis.InnerProductSpace.Trace	2365	2370	+5 (+0.21%)

Import changes for all files

Files	Import difference
Mathlib.Analysis.InnerProductSpace.SingularValues	2
9 files Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.Reproducing Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Moments.CovarianceBilin	4
Mathlib.Analysis.InnerProductSpace.Trace	5
6 files Mathlib.Analysis.Matrix.HermitianFunctionalCalculus Mathlib.Analysis.Matrix.LDL Mathlib.Analysis.Matrix.Order Mathlib.Analysis.Matrix.PosDef Mathlib.Analysis.Matrix.Spectrum Mathlib.Combinatorics.SimpleGraph.LapMatrix	8
Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Analysis.InnerProductSpace.Spectrum	9
Mathlib.LinearAlgebra.Eigenspace.Charpoly	59

---

Declarations diff

+ charpoly_eq
+ det_eq_prod_eigenvalues
+ det_eq_prod_roots_charpoly_of_splits
+ eigenvalues_eq_eigenvalues_iff
+ roots_charpoly_eq_eigenvalues
+ sort_roots_charpoly_eq_eigenvalues
+ splits_charpoly
+ toMatrix_eigenvectorBasis
+ trace_eq_sum_roots_charpoly_of_splits

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).

[wwylele]

t-analysis

[themathqueen]

LGTM except this tiny comment, let's see what Jireh thinks about it.

(apparently, both your PR and the matrix version #29476 used the Aristotle-Harmonic bot 👀)

[j-loreaux]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step