Commit 2024-08-20 19:19 f904bf86

View on Github →

chore: Better names for (⌊a⌋₊ : α) = ⌊a⌋ again (#16001) Also remove the six months old deprecated names

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added theorem Int.natCast_ceil_eq_ceil

added theorem Int.natCast_floor_eq_floor

deleted theorem Int.ofNat_ceil_eq_ceil

deleted theorem Int.ofNat_floor_eq_floor