Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-25 18:07 b059a442

View on Github →

feat(algebra/order/floor): lemmas about int.floor, int.ceil, int.fract, round (#16158)

Estimated changes

added theorem abs_sub_round_eq_min
added theorem int.abs_fract
added theorem int.abs_one_sub_fract
deleted theorem int.ceil_coe
added theorem int.ceil_int_cast
added theorem int.ceil_nat_cast
modified theorem int.ceil_one
added theorem int.ceil_sub_self_eq
modified theorem int.ceil_zero
deleted theorem int.floor_coe
added theorem int.floor_int_cast
added theorem int.floor_nat_cast
modified theorem int.floor_one
modified theorem int.floor_zero
deleted theorem int.fract_coe
modified theorem int.fract_floor
added theorem int.fract_int_cast
added theorem int.fract_nat_cast
modified theorem int.fract_nonneg
modified theorem int.lt_floor_add_one
added theorem int.one_le_ceil_iff
modified theorem int.sub_one_lt_floor
modified def round
added theorem round_eq
added theorem round_int_cast
added theorem round_nat_cast
modified theorem round_one
modified theorem round_zero
added theorem int.pos_iff_one_le
added theorem max_def'
added theorem min_def'