Mathlib Changelog
v4
Changelog
About
Github
Theorem
Nat.cast_mul_floor_div_cancel
Modification history
2025-08-27 10:43
Mathlib/Algebra/Order/Floor/Semifield.lean
refactor: add `assert_not_exists Field` to `Mathlib.Combinatorics.SimpleGraph.Extremal.Basic` (#28721) …
Modified
Nat.cast_mul_floor_div_cancel
View on Github →
2025-07-02 03:08
Mathlib/Algebra/Order/Floor/Semiring.lean
feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` (#26004) …
Added
Nat.cast_mul_floor_div_cancel
View on Github →