diff --git a/Mathlib/NumberTheory/LocalField/Basic.lean b/Mathlib/NumberTheory/LocalField/Basic.lean
index a36451a54dc070..77195e61c23342 100644
--- a/Mathlib/NumberTheory/LocalField/Basic.lean
+++ b/Mathlib/NumberTheory/LocalField/Basic.lean
@@ -126,6 +126,12 @@ def valueGroupWithZeroIsoInt : ValueGroupWithZero K ≃*o ℤᵐ⁰ := by
     (Units.map_injective (f := e.symm.toMonoidHom) e.symm.injective).nontrivial
   exact ⟨e.symm.trans (LocallyFiniteOrder.orderMonoidWithZeroEquiv _)⟩
 
+instance : IsCyclic (ValueGroupWithZero K)ˣ :=
+  (Units.mapEquiv (valueGroupWithZeroIsoInt K).toMulEquiv).isCyclic.mpr inferInstance
+
+instance : Nontrivial (ValueGroupWithZero K)ˣ :=
+  ValuativeRel.isNontrivial_iff_nontrivial_units.mp inferInstance
+
 instance : ValuativeRel.IsDiscrete K :=
   (ValuativeRel.nonempty_orderIso_withZeroMul_int_iff.mp ⟨valueGroupWithZeroIsoInt K⟩).1