no goals
R : Type u_1
inst✝ : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ ↑(RingEquiv.symm (opRingEquiv R)) (↑C r * X ^ n) = op (↑C (unop r) * X ^ n)
rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]