Commit 2026-10-29 02:16 d0207795

View on Github →

refactor(Algebra/Order): unbundle group and ring cone (#37298)

  • Unbundle GroupCone and RingCone using Submonoid.IsMulPointed This PR deprecates the GroupCone and RingCone structures, making use of the predicates Submonoid.IsMulPointed and AddSubmonoid.IsPointed defined in that file instead. These predicates allow us to treat uniformly
  • positive cones in groups and rings
  • pointed cones in vector spaces over an ordered field
  • orderings in rings This reduces duplication of theorems. Unbundling group and ring cones is further justified by the principle that there are no new operations on them: they correspond to operations on the underlying submonoids and subsemirings, respectively. See the discussion at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/When.20should.20subobjects.20be.20bundled.3F/with/609099816 See also #36863 for the analogous change to ring orderings.

Estimated changes

modified theorem RingCone.coe_nonneg
modified theorem RingCone.mem_nonneg