Commit 2024-09-23 12:22 9a329fb9

View on Github →

feat: ⌈a⌉ < 2 * a (#17024) From LeanAPAP

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added theorem Int.ceil_div_ceil_inv_sub_one

added theorem Int.ceil_le_mul

added theorem Int.ceil_le_two_mul

added theorem Int.ceil_lt_iff

added theorem Int.ceil_lt_mul

added theorem Int.ceil_lt_two_mul

added theorem Int.div_two_lt_floor

added theorem Int.le_ceil_iff

added theorem Int.mul_lt_floor

added theorem Nat.ceil_le_mul

added theorem Nat.ceil_le_two_mul

added theorem Nat.ceil_lt_mul

added theorem Nat.ceil_lt_two_mul

added theorem Nat.div_two_lt_floor

added theorem Nat.mul_lt_floor

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