∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F} [inst_1 : Decidable (q = 0)] (hpq : p ∣ q),
  Polynomial.Gal.restrictDvd hpq = if hq : q = 0 then 1 else Polynomial.Gal.restrict p q.SplittingField