a^{-1} < 0

Stream: mathlib4

[Yury G. Kudryashov]

Currently, docs#inv_neg'' (a.k.a. docs#inv_lt_zero) assumes that the type is a linearly ordered group with zero. The same lemma is true in a partially ordered field (actually, a division semiring with docs#ExistsAddOfLE). The latter version (not in Mathlib) includes, e.g., complex numbers (and probably quaternions, but we have no PartialOrder instance there and I didn't verify the details). Are there any linear ordered groups with zero that (a) we care about; (b) aren't division semirings?

[Yury G. Kudryashov]

If yes, should I add a typeclass InvLTZero and provide instances for GroupWithZero and DivisionSemiring?

[Kevin Buzzard]

WithZero (Multiplicative Int) is so popular in valuation theory that we even have notation ℤₘ₀ for it.

[Yury G. Kudryashov]

But you have no negative elements there.

[Kevin Buzzard]

Yes, in valuation theory 0 is always bot for the target monoid.

[Yaël Dillies]

In my mind, either you adjoin a zero to a group and everything is nonnegative, or you were in a field to start with. So restricting to DivisionSemiring sounds fine to me