Mathlib Changelog
v4
Changelog
About
Github
Theorem
Int.mul_cast_floor_div_cancel_of_pos
Modification history
2025-07-02 03:08
Mathlib/Algebra/Order/Floor/Ring.lean
feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` (#26004) …
Added
Int.mul_cast_floor_div_cancel_of_pos
View on Github →