Characteristic polynomial of polynomial of matrix

Stream: Is there code for X?

[Bhavik Mehta]

Do we have anything like

import Mathlib

example {n : Type*} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (p : Polynomial ℝ)
    (μ : n → ℝ) (h : A.charpoly = ∏ i, (X - C (μ i))) :
    (p.eval₂ (Matrix.scalar _) A).charpoly = ∏ i, (X - C (p.eval (μ i))) := by

This corresponds to the Theorem here: https://en.wikipedia.org/wiki/Characteristic_polynomial#Characteristic_polynomial_of_Ak, whose proof is given by matrix decomposition (either Schur or Jordan works). Do we have anything close to either of these?
Note that while I'm happy to assume the characteristic polynomial splits and the algebraic and geometric multiplicities agree, I can't assume that eigenvalues are distinct in my application.

[Jireh Loreaux]

Related, but not what you want exactly: docs#spectrum.map_polynomial_aeval_of_degree_pos

[Bhavik Mehta]

Yeah this is close, but unfortunately I don't think I can make it helpful in my application - I have very many repeated eigenvalues and I really do need to know that multiplicities are preserved.

[Jireh Loreaux]

Right, it's certainly not a drop-in, but it's possible that parts of the argument are helpful (potentially also not).