no goals
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ ↑(opRingEquiv R) (op (↑C r * X ^ n)) = ↑C (op r) * X ^ n
simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]