Commit 2025-07-02 03:08 3675c9af

View on Github →

feat(Algebra/Order/Floor): ⌊n * x⌋₊ / n = ⌊x⌋₊ (#26004) Prove that ⌊n * x⌋₊ / n = ⌊x⌋₊ for natural n.

Estimated changes

Modified Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

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

added theorem Int.cast_mul_floor_div_cancel_of_pos

added theorem Int.floor_div_cast_of_nonneg

added theorem Int.floor_div_natCast

added theorem Int.mul_cast_floor_div_cancel_of_pos

added theorem Int.mul_natCast_floor_div_cancel

added theorem Int.natCast_mul_floor_div_cancel

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

added theorem Nat.cast_mul_floor_div_cancel

added theorem Nat.mul_cast_floor_div_cancel

Modified Mathlib/Data/EReal/Inv.lean