Theorems · Theorem · order theory
LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered
∀ (G : Type u_2) [inst : LinearOrderedCommGroupWithZero G] [Nontrivial Gˣ] [MulArchimedean G], Nonempty (G ≃*o WithZero (Multiplicative ℤ)) ↔ ¬DenselyOrdered G
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, exclusively
- Defined in
- Mathlib.GroupTheory.ArchimedeanDensely
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites35
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Equiv.symmproof · cited by 3,681
- Unitsstatement and proof · cited by 2,804
- Nontrivialstatement and proof · cited by 2,416
- Units.valproof · cited by 1,966
- map_zeroproof · cited by 1,614
- Multiplicativestatement and proof · cited by 875
- WithZerostatement and proof · cited by 586
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- MulEquiv.symmproof · cited by 482
- DenselyOrderedstatement · cited by 471
- MonoidHomClass.toMonoidHomproof · cited by 294
Cited by4
Results whose statement or proof uses this declaration.
- ValuativeRel.nonempty_orderIso_withZeroMul_int_iffproof · cited by 1
- Valuation.Integers.isPrincipalIdealRing_iff_not_denselyOrderedproof · cited by 1
- ValuativeRel.IsDiscrete.of_compatible_withZeroMulIntproof · cited by 0
- not_denselyOrdered_withZero_intproof · cited by 0