no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
r : R
k : ℕ
⊢ content (↑(monomial k) r) = ↑normalize r
rw [← C_mul_X_pow_eq_monomial, content_C_mul, content_X_pow, mul_one]