Commit 2024-06-09 09:51 76e09972
View on Github →chore: Move the inheritance StrictOrderedSemiring α → CharZero α
instance to a less obscure file (#13654)
There is little point in avoiding to import CharZero
in Algebra.Order.Ring.Defs
(where StrictOrderedSemiring
is defined) since it is so basic. Exiling the titular basic instance to an obscure file meant that people had trouble finding that instance (and it just happened to Eric).