no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : IsPrimitive p
hq : IsPrimitive q
⊢ IsPrimitive (p * q)
rw [isPrimitive_iff_content_eq_one, content_mul, hp.content_eq_one, hq.content_eq_one, mul_one]