feat(GroupTheory/ArchimedeanDensely): linear ordered group subsets are WF if discrete

[pechersky]

---

• depends on: feat(Order/Interval/Finset/Defs): transfer LocallyFiniteOrder  #18479
• depends on: feat(Order/WellFoundedOn): wfon.mapsTo and sdff_singleton #18480

[github-actions]

PR summary d7f001f8ca

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.ArchimedeanDensely	790	791	+1 (+0.13%)

Import changes for all files

Files	Import difference
Mathlib.GroupTheory.ArchimedeanDensely	1

---

Declarations diff

+ LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete
+ LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
+ LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete
+ LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
+ LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero
+ LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero
+ LocallyFiniteOrder.ofOrderIsoClass
+ WellFoundedOn.mapsTo
+ WellFoundedOn.sdiff_singleton
+ inv_apply_eq_iff_eq_apply
+ wellFoundedOn_sdiff_singleton

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• feat(Order/Interval/Finset/Defs): transfer LocallyFiniteOrder  #18479
• feat(Order/WellFoundedOn): wfon.mapsTo and sdff_singleton #18480
  By Dependent Issues (🤖). Happy coding!