R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsRadical 0
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
x : R
⊢ x = 0 → IsRadical x
rintro rfl
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsReduced R
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsRadical 0
rw [zero_isRadical_iff]
no goals
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : GCDMonoid R
⊢ IsReduced R
infer_instance