Commit 2026-03-18 12:31 a28e6110

View on Github →

feat(Algebra/Order/Floor/Ring): generalize Int.abs_sub_lt_one_of_floor_eq_floor (#36805) This PR weakens the CommRing R assumption on Int.abs_sub_lt_one_of_floor_eq_floor into Ring R.

Estimated changes