Commit 2024-07-16 22:43 126510dd

chore (Algebra.Order.Ring.Defs): split file and unbundle results (#14393) All of the theorems in Algebra.Order.Ring.Defs currently take bundled ordered algebraic typeclasses, eg OrderedSemiring as paramaters unecessarily. We unbundle the results keeping the algebra and order data/theorems separate and adding the mixin compatbility typeclasses as needed and place the theorems in Algebra.Order.Ring.Unbundled.Basic. As Algebra.Order.Ring.Defs and upstream resuls already allow us to pass from bundled classes to unbundled classes appropriately, we lose no uusability by doing this. We lessen dependecies and gain future flexibility.