Commit 2025-11-26 10:04 ce7caf17

View on Github →

feat(Algebra/Order/Floor): generalize mul_floor_div theorems to rings and semirings (#30041) Generalize mul_cast_floor_div_cancel from Field and Semifield to Ring and Semiring.

Estimated changes

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

modified theorem Int.cast_mul_floor_div_cancel_of_pos

modified theorem Int.mul_cast_floor_div_cancel_of_pos

modified theorem Int.mul_natCast_floor_div_cancel

modified theorem Int.natCast_mul_floor_div_cancel

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

deleted theorem Nat.cast_mul_floor_div_cancel

deleted theorem Nat.mul_cast_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/Analysis/Real/OfDigits.lean