Polynomial cast

Stream: Is there code for X?

[Edison Xie]

If I have an algebra instance Algebra K F where K and F are fields, how do I cast an element in K[X] to F[X]? More specifically, if I want to prove an element f in F[X] is actually "in" K[X], how should I make the statement?

[Edison Xie]

import Mathlib

open scoped TensorProduct

open Polynomial

suppress_compilation

variable (K F : Type*) (n : ℕ) [Field K] [Field F] [Algebra K F] (A : CSA K)
    (e : F ⊗[K] A ≃ₐ[K] Matrix (Fin n) (Fin n) F)

variable {K F n} in
def ReducedCharPoly (a : A): Polynomial F := Matrix.charpoly (e (1 ⊗ₜ a))

namespace ReducedCharPoly

lemma mem_Kx (a : A) : ∃ f : K[X], ReducedCharPoly A e a =
    ∑ i : Fin (ReducedCharPoly A e a).natDegree, f.coeff i.1 • X^i.1 := sorry

end ReducedCharPoly

[Edison Xie]

this is what I'm currently using but I feel like there should be better expressions for this lemma?

[Eric Wieser]

docs#Polynomial.map with algebraMap?