Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-12 07:31 cb1b6d97

View on Github →

feat(algebra/order/floor): adds some missing floor API (#11336)

Estimated changes

Modified src/algebra/order/floor.lean

modified theorem int.ceil_to_nat

modified theorem int.floor_to_nat

added theorem nat.cast_ceil_eq_cast_int_ceil

added theorem nat.cast_ceil_eq_int_ceil

added theorem nat.cast_floor_eq_cast_int_floor

added theorem nat.cast_floor_eq_int_floor

added theorem nat.floor_le_of_le