∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], Nonempty (ValuativeRel.ValueGroupWithZero K ≃*o WithZero (Multiplicative ℤ))