Theorem Nat.cast_mul_floor_div_cancel

Modification history

2025-11-26 10:04
Mathlib/Algebra/Order/Floor/Semifield.lean
feat(Algebra/Order/Floor): generalize mul_floor_div theorems to rings and semirings (#30041) …
Modified Nat.cast_mul_floor_div_cancelView on Github →
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_cancelView 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_cancelView on Github →