Commit 2026-01-08 11:26 4ca1c2ea

refactor: make LinearOrderedCommMonoidWithZeros cancellative (#31749) It appears that the only interesting LinearOrderedCommMonoidWithZeros are the ones for which every non-zero element is regular. This PR therefore strenghtens LinearOrderedCommMonoidWithZero, and similarly for LinearOrderedAddCommMonoidWithTop, its additive counterpart. Here are the instances we lose:

• ENNReal: multiplication by \top isn't injective
• ERealᵒᵈ: multiplication by \top isn't injective
• Cardinal: multiplication by anything but 1 isn't injective
• ArchimedeanClass R where R is a non-strict ordered ring
• the pathological counterexample of a LinearOrderedCommMonoidWithZero where two positive numbers multiply to zero I believe these are all fine to lose since they had no mathematical motivation (we never use those as targets of valuations). There is an argument to be made that we could keep the existing typeclass as is and instead have the one I'm currently replacing it with under the name LinearOrderedCancelCommMonoidWithZero. There are at least two reasons I do not want to do this:

1. We have no evidence that the weaker typeclass is actually useful
2. LinearOrderedCommMonoidWithZero, weak or strong version, extends both the algebra and order hierarchy, which is something we want to move away from. Therefore, if anything, we should not be adding more of those typeclasses. This will be used in a later PR to replace pow_eq_one_iff with IsMulTorsionFree.pow_eq_one_iff_left. Zulip