Commit 2024-11-08 20:24 2f529a27

View on Github →

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

Estimated changes

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete

added theorem LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete

added theorem LinearOrderedCommGroup.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete

added theorem LinearOrderedCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete

added theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_ge_gt_iff_nonempty_discrete_of_ne_zero

added theorem LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero