LinearOrderedAddCommGroup no longer exists

Stream: new members

[Kevin Cheung]

I am trying to update some old code (written for v4.3.0) to work with v4.26.0. The code has [LinearOrderedAddCommGroup G]. Lean complains that it is invalid binder annotation.

Looking inside Mathlib/Algebra/Order/Group/Defs.lean I see

-- `LinearOrderedCommGroup` and `LinearOrderedAddCommGroup` no longer exist, but we still use the namespaces.

I'm not sure what that means. In any case, what should I replace [LinearOrderedAddCommGroup G] with?

[Bbbbbbbbba]

[AddCommGroup G] [LinearOrder G]?

[Stepan Nesterov]

Probably [IsOrderedAddMonoid G] [Group G] [LinearOrder G] (we need a compatibility of order and multiplication)

[Junyan Xu]

IsOrderedAddMonoid needs to come at the end

[Eric Wieser]

Did we go through a deprecation cycle here?

[Kevin Cheung]

Looks like the following works:

 lemma IneqExtra.neg_le_sub_self_of_nonneg {G} [LinearOrder G] [AddCommGroup G] [IsOrderedAddMonoid G] {a b : G} (h : 0 ≤ a) :
    -b ≤ a - b := by
  rw [sub_eq_add_neg]
  apply le_add_of_nonneg_left h

Originally, it was

lemma IneqExtra.neg_le_sub_self_of_nonneg [LinearOrderedAddCommGroup G] {a b : G} (h : 0 ≤ a) :
    -b ≤ a - b := by
  rw [sub_eq_add_neg]
  apply le_add_of_nonneg_left h

[Kevin Cheung]

Not sure if the modification is the correct one.

[Junyan Xu]

deprecated 2025-04-10, removed 2025-10-21
https://github.com/leanprover-community/mathlib4/pull/30759/files#diff-1ea79e1c68d33cde0e0d03b5cd88acada0fe81a37be3c91e0dbdf5734e81b824L81-L83
Lean v4.3.0 was 2023-11-16 ...

[Kevin Cheung]

Thank you!