Commit 2024-02-15 01:43 1297e8b5

View on Github →

chore: Better names for (⌊a⌋₊ : α) = ⌊a⌋ (#10252) The new lemma names are more symmetric, hence hopefully more discoverable

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added theorem Int.ofNat_ceil_eq_ceil

added theorem Int.ofNat_floor_eq_floor

deleted theorem Nat.cast_ceil_eq_cast_int_ceil

deleted theorem Nat.cast_ceil_eq_int_ceil

deleted theorem Nat.cast_floor_eq_cast_int_floor

deleted theorem Nat.cast_floor_eq_int_floor

added theorem natCast_ceil_eq_intCast_ceil

added theorem natCast_floor_eq_intCast_floor