Commit 2024-07-16 22:43 126510dd
View on Github →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.