feat(GroupTheory/Archimedean): `LinearOrderedCommGroupWithZero.discre…

…te_or_denselyOrdered` (#15846)

Co-authored-by: Yakov Pechersky <[email protected]>

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -427,3 +427,8 @@ instance (priority := 100) FloorRing.archimedean (α) [LinearOrderedField α] [F
     Archimedean α := by
   rw [archimedean_iff_int_le]
   exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩
+
+@[to_additive]
+instance Units.instMulArchimedean (α) [OrderedCommMonoid α] [MulArchimedean α] :
+    MulArchimedean αˣ :=
+  ⟨fun x {_} h ↦ MulArchimedean.arch x.val h⟩

Mathlib/GroupTheory/ArchimedeanDensely.lean

@@ -21,7 +21,7 @@ They are placed here in a separate file (rather than incorporated as a continuat
 `GroupTheory.Archimedean`) because they rely on some imports from pointwise lemmas.
 -/
 
-open Set
+open Multiplicative Set
 
 -- no earlier file imports the necessary requirements for the next two
 
@@ -210,3 +210,36 @@ lemma LinearOrderedCommGroup.discrete_or_denselyOrdered :
   refine (LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)).imp ?_ id
   rintro ⟨f, hf⟩
   exact ⟨AddEquiv.toMultiplicative' f, hf⟩
+
+/-- Any nontrivial (has other than 0 and 1) linearly ordered mul-archimedean group with zero is
+either isomorphic (and order-isomorphic) to `ℤₘ₀`, or is densely ordered. -/
+lemma LinearOrderedCommGroupWithZero.discrete_or_denselyOrdered (G : Type*)
+    [LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G] :
+    Nonempty (G ≃*o ℤₘ₀) ∨ DenselyOrdered G := by
+  classical
+  refine (LinearOrderedCommGroup.discrete_or_denselyOrdered Gˣ).imp ?_ ?_
+  · intro ⟨f⟩
+    refine ⟨OrderMonoidIso.trans
+      ⟨WithZero.withZeroUnitsEquiv.symm, ?_⟩ ⟨f.withZero, ?_⟩⟩
+    · intro
+      simp only [WithZero.withZeroUnitsEquiv, MulEquiv.symm_mk,
+        MulEquiv.toEquiv_eq_coe, Equiv.toFun_as_coe, EquivLike.coe_coe, MulEquiv.coe_mk,
+        Equiv.coe_fn_symm_mk ]
+      split_ifs <;>
+      simp_all [← Units.val_le_val]
+    · intro a b
+      induction a <;> induction b <;>
+      simp [MulEquiv.withZero]
+  · intro H
+    refine ⟨fun x y h ↦ ?_⟩
+    rcases (zero_le' (a := x)).eq_or_lt with rfl|hx
+    · lift y to Gˣ using h.ne'.isUnit
+      obtain ⟨z, hz⟩ := exists_ne (1 : Gˣ)
+      refine ⟨(y * |z|ₘ⁻¹ : Gˣ), ?_, ?_⟩
+      · simp [zero_lt_iff]
+      · rw [Units.val_lt_val]
+        simp [hz]
+    · obtain ⟨z, hz, hz'⟩ := H.dense (Units.mk0 x hx.ne') (Units.mk0 y (hx.trans h).ne')
+        (by simp [← Units.val_lt_val, h])
+      refine ⟨z, ?_, ?_⟩ <;>
+      simpa [← Units.val_lt_val]