R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), ↑C r ∣ p → IsUnit r) ↔ IsUnit (content p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ IsPrimitive p ↔ content p = 1
rw [← normalize_content, normalize_eq_one, IsPrimitive]
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ content p → IsUnit r) ↔ IsUnit (content p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), ↑C r ∣ p → IsUnit r) ↔ IsUnit (content p)
simp_rw [← dvd_content_iff_C_dvd]
no goals
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
⊢ (∀ (r : R), r ∣ content p → IsUnit r) ↔ IsUnit (content p)
exact ⟨fun h => h p.content (dvd_refl p.content), fun h r hdvd => isUnit_of_dvd_unit hdvd h⟩