Commit 2026-04-06 13:59 03cf4f1c

View on Github →

feat: weaken assumptions on lemmas about FloorRing (#37582) This PR weakens the assumptions on lemmas about FloorSemiring and FloorRing, mostly from IsStrictOrderedRing to IsOrderedRing. A few lemmas requiring commutativity on the ring are also modified to drop the commutativity assumption.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Defs.lean

modified def FloorRing.ofCeil

modified def FloorRing.ofFloor

modified theorem Int.ceil_nonneg

modified theorem Int.floor_nonpos

Modified Mathlib/Algebra/Order/Floor/Ring.lean

modified theorem Int.ceil_eq_on_Ioc'

Modified Mathlib/Algebra/Order/Floor/Semifield.lean

Modified Mathlib/Algebra/Order/Floor/Semiring.lean

modified theorem Nat.cast_mul_floor_div_cancel

modified theorem Nat.ceil_intCast