Commit 2024-10-18 15:48 8b31f1fb

View on Github →

feat(GroupTheory/ArchimedeanDensely): discrete iff not densely ordered (#16618) Stronger statements than previously proven Ors

Estimated changes

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered

added theorem LinearOrderedCommGroup.discrete_iff_not_denselyOrdered

added theorem LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered

added theorem denselyOrdered_units_iff