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).

Estimated changes