Commit 2022-11-01 22:54 243f55c8
View on Github →chore(init/data/int): move lemmas (#525)
The file Init.Data.Int.Basic
contained three declarations:
Int.LinearOrder
Int.coe_nat_le
Int.coe_nat_lt
In mathlib3 all three of these were in other files: the first inInit.Data.Int.Order
and the two last inData.Int.Basic
. I propose moving them to the corresponding mathlib4 files so that people know where to look for them. Zulip