Commit 2026-06-03 13:03 34e41cb1

View on Github →

feat(Algebra/Order/Floor/Defs): Nat.cast is strictly monotone in FloorSemiring and FloorRing (#37714) As title says, and without the IsOrderedRing assumption. Other than that, I removed the IsOrderedRing assumption from pretty much all the lemmas in Algebra/Order/Floor/Defs that could possibly have this assumption removed, and reduced some IsStrictOrderedRing assumptions to IsOrderedRing + Nontrivial. Due to strict monotonicity, we can also provide CharZero instance on FloorSemiring and FloorRing. Thus we can remove the NeZero and Nontrivial instances on them. The changes on /Ring and /Semiring are trivial changes due to some lemmas not requiring an IsOrderedRing instance anymore.

Estimated changes

added theorem FloorRing.intCast_mono
added theorem Int.ceil_lt_iff
modified theorem Int.ceil_nonneg
added theorem Int.ceil_nonpos
added theorem Int.floor_le_iff
added theorem Int.floor_lt_zero
modified theorem Int.floor_nonpos
added theorem Int.le_ceil_iff
added theorem Int.lt_floor_iff
modified theorem Nat.le_floor
modified theorem exists_floor'
deleted theorem Int.ceil_lt_iff
deleted theorem Int.floor_le_iff
deleted theorem Int.le_ceil_iff
deleted theorem Int.lt_floor_iff