no goals
R : Type u_1
S : Type u_2
q : R
n : ℕ
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
⊢ eval (↑f q) (cyclotomic n S) = ↑f (eval q (cyclotomic n R))
rw [← map_cyclotomic n f, eval_map, eval₂_at_apply]