no goals
R : Type ?u.236266
S : Type u_2
T : Type ?u.236272
inst✝¹⁰ : CommRing R
inst✝⁹ : Ring S
inst✝⁸ : Algebra R S
A : Type u_1
B : Type ?u.236578
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : Algebra A B
K : Type ?u.237000
inst✝³ : Field K
inst✝² : Algebra A S
S' : Type u_3
inst✝¹ : Ring S'
inst✝ : Algebra A S'
pb : PowerBasis A S
y : S'
hy : ↑(aeval y) (minpoly A pb.gen) = 0
x : A
⊢ ↑(↑(Basis.constr pb.basis A) fun i => y ^ ↑i) (↑(algebraMap A S) x) = ↑(algebraMap A S') x
convert pb.constr_pow_aeval hy (C x) <;> rw [aeval_C]