Commit 2024-05-28 16:14 3185f99d
View on Github →chore: Do not import order theory in Data.Int.Cast.Lemmas
(#13305)
Split off the lemmas about OrderedRing
from Data.Int.Cast.Lemmas
to a new file Algebra.Order.Ring.Cast
.
chore: Do not import order theory in Data.Int.Cast.Lemmas
(#13305)
Split off the lemmas about OrderedRing
from Data.Int.Cast.Lemmas
to a new file Algebra.Order.Ring.Cast
.