diff --git a/src/ring_theory/adjoin_root.lean b/src/ring_theory/adjoin_root.lean
index f548e2fc730b2..efb922d502378 100644
--- a/src/ring_theory/adjoin_root.lean
+++ b/src/ring_theory/adjoin_root.lean
@@ -322,7 +322,7 @@ noncomputable instance field [fact (irreducible f)] : field (adjoin_root f) :=
   qsmul_eq_mul' := λ a x, adjoin_root.induction_on _ x (λ p,
     by { rw [smul_mk, of, ring_hom.comp_apply, ← (mk f).map_mul, polynomial.rat_smul_eq_C_mul] }),
   ..adjoin_root.comm_ring f,
-  ..ideal.quotient.field (span {f} : ideal K[X]) }
+  ..ideal.quotient.group_with_zero (span {f} : ideal K[X]) }
 
 lemma coe_injective (h : degree f ≠ 0) : function.injective (coe : K → adjoin_root f) :=
 have _ := adjoin_root.nontrivial f h, by exactI (of f).injective