Commit 2025-02-11 10:15 81f35f27

View on Github →

feat(Algebra/Order): characterize floor a and ceil a based on whether a is integer (#21648)

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added theorem Int.ceil_eq_floor_add_one_iff_not_mem

added theorem Int.ceil_eq_self_iff_mem

added theorem Int.floor_eq_self_iff_mem