Commit 2026-01-23 08:59 eeb7b546

refactor(Algebra/Order/Field/Basic): generalize file from LinearOrder to PartialOrder and PosMulReflectLT (#33100) It's a well-known easy fact that there is no way to equip ℂ with a linear order satisfying IsStrictOrderedRing. However, it is equipped with a partial order (available in the ComplexOrder namespace) given by a ≤ b ↔ a.re ≤ b.re ∧ a.im = b.im. This order satisfies IsStrictOrderedRing. However, it has some other nice properties, for instance 0 < a⁻¹ ↔ 0 < a (because it is a GroupWithZero satisfying PosMulReflectLT so inv_pos applies), and moreover, in this PR we also show that a (partially) ordered field with this property satisfies a⁻¹ < 0 ↔ a < 0. This means that the field operation is well-behaved in regards to elements comparable with zero. This PR refactors Algebra/Order/Field/Basic.lean so that it applies to partially ordered fields that in addition satisfy PosMulReflectLT (e.g., ℂ). The vast majority of the lemmas are applicable in this more general setting, albeit with refactored proofs. The diff is a bit messy, but it's easy to understand with the right point-of-view:

1. lemmas which require linear orders are grouped into their own sections below the corresponding sections for partially ordered fields
2. proofs are refactored with the weaker hypotheses
3. a few lemmas near the top didn't actually need IsStrictOrderedRing, so those are grouped at the top.
4. The only new declarations added are inv_lt_zero' and inv_nonpos', no others were deleted or changed (aside from weakening type class assumptions).
5. The positivity extension at the bottom of the file has its type class requirements weakened so that it applies in more contexts.