Skip to content

Commit

Permalink
Update Mathlib/GroupTheory/ArchimedeanDensely.lean
Browse files Browse the repository at this point in the history
Co-authored-by: Jz Pan <[email protected]>
  • Loading branch information
pechersky and acmepjz authored Oct 31, 2024
1 parent 031384b commit d7f001f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/GroupTheory/ArchimedeanDensely.lean
Original file line number Diff line number Diff line change
Expand Up @@ -299,7 +299,7 @@ lemma LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered (G : Type*)
split_ifs <;>
simp_all [← Units.val_le_val]

section WellFounded
section WellFounded

lemma LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete
{G : Type*} [LinearOrderedAddCommGroup G] [Nontrivial G] {g : G} :
Expand Down

0 comments on commit d7f001f

Please sign in to comment.