R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ IsUnit (coeff p 0)
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ IsUnit p
rw [eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm), isUnit_C]
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ ↑C (coeff p 0) ∣ p * q
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ IsUnit (coeff p 0)
refine' hu _ _
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ p ∣ p * q
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ ↑C (coeff p 0) ∣ p * q
rw [← eq_C_of_degree_le_zero (natDegree_eq_zero_iff_degree_le_zero.1 hpm)]
no goals
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hu : IsPrimitive (p * q)
hpm : natDegree p = 0
⊢ p ∣ p * q
exact dvd_mul_right _ _