Theorem: Polynomial.C_eq_smul_one (DividedPowers/IdealAdd.lean)

State before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ C a = a • 1
Tactic:
rw [← C_mul', mul_one]
State after:
no goals