Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-14 13:24 9da33a89

View on Github →

refactor(algebra/floor): Rename floor and ceil functions (#9590) This renames

  • floor -> int.floor
  • ceil -> int.ceil
  • fract -> int.fract
  • nat_floor -> nat.floor
  • nat_ceil -> nat.ceil

Estimated changes

deleted def ceil
deleted theorem ceil_add_int
deleted theorem ceil_coe
deleted theorem ceil_eq_iff
deleted theorem ceil_eq_on_Ioc'
deleted theorem ceil_eq_on_Ioc
deleted theorem ceil_le
deleted theorem ceil_le_floor_add_one
deleted theorem ceil_lt_add_one
deleted theorem ceil_mono
deleted theorem ceil_nonneg
deleted theorem ceil_pos
deleted theorem ceil_sub_int
deleted theorem ceil_zero
deleted def floor
deleted theorem floor_add_fract
deleted theorem floor_add_int
deleted theorem floor_add_nat
deleted theorem floor_coe
deleted theorem floor_eq_iff
deleted theorem floor_eq_on_Ico'
deleted theorem floor_eq_on_Ico
deleted theorem floor_fract
deleted theorem floor_int_add
deleted theorem floor_le
deleted theorem floor_lt
deleted theorem floor_lt_ceil_of_lt
deleted theorem floor_mono
deleted theorem floor_nat_add
deleted theorem floor_nonneg
deleted theorem floor_one
deleted theorem floor_pos
deleted theorem floor_sub_int
deleted theorem floor_sub_nat
deleted theorem floor_zero
deleted def fract
deleted theorem fract_add
deleted theorem fract_add_floor
deleted theorem fract_coe
deleted theorem fract_eq_fract
deleted theorem fract_eq_iff
deleted theorem fract_floor
deleted theorem fract_fract
deleted theorem fract_lt_one
deleted theorem fract_mul_nat
deleted theorem fract_nonneg
deleted theorem fract_zero
added def int.ceil
added theorem int.ceil_add_int
added theorem int.ceil_coe
added theorem int.ceil_eq_iff
added theorem int.ceil_eq_on_Ioc'
added theorem int.ceil_eq_on_Ioc
added theorem int.ceil_le
added theorem int.ceil_lt_add_one
added theorem int.ceil_mono
added theorem int.ceil_nonneg
added theorem int.ceil_pos
added theorem int.ceil_sub_int
added theorem int.ceil_zero
added def int.floor
added theorem int.floor_add
added theorem int.floor_add_fract
added theorem int.floor_add_int
added theorem int.floor_add_nat
added theorem int.floor_coe
added theorem int.floor_eq_iff
added theorem int.floor_eq_on_Ico'
added theorem int.floor_eq_on_Ico
added theorem int.floor_fract
added theorem int.floor_int_add
added theorem int.floor_le
added theorem int.floor_lt
added theorem int.floor_mono
added theorem int.floor_nonneg
added theorem int.floor_one
added theorem int.floor_pos
added theorem int.floor_sub_int
added theorem int.floor_sub_nat
added theorem int.floor_zero
added def int.fract
added theorem int.fract_add
added theorem int.fract_add_floor
added theorem int.fract_coe
added theorem int.fract_eq_fract
added theorem int.fract_eq_iff
added theorem int.fract_floor
added theorem int.fract_fract
added theorem int.fract_lt_one
added theorem int.fract_mul_nat
added theorem int.fract_nonneg
added theorem int.fract_zero
added theorem int.le_ceil
added theorem int.le_floor
added theorem int.lt_ceil
added theorem int.lt_floor_add_one
added theorem int.lt_succ_floor
added theorem int.sub_one_lt_floor
deleted theorem le_ceil
deleted theorem le_floor
deleted theorem le_nat_ceil
deleted theorem le_nat_floor_iff
deleted theorem le_nat_floor_of_le
deleted theorem le_of_nat_ceil_le
deleted theorem lt_ceil
deleted theorem lt_floor_add_one
deleted theorem lt_nat_ceil
deleted theorem lt_nat_floor_add_one
deleted theorem lt_of_lt_nat_floor
deleted theorem lt_of_nat_ceil_lt
deleted theorem lt_succ_floor
added def nat.ceil
added theorem nat.ceil_add_nat
added theorem nat.ceil_coe
added theorem nat.ceil_eq_zero
added theorem nat.ceil_le
added theorem nat.ceil_lt_add_one
added theorem nat.ceil_mono
added theorem nat.ceil_zero
added def nat.floor
added theorem nat.floor_add_nat
added theorem nat.floor_coe
added theorem nat.floor_eq_zero_iff
added theorem nat.floor_le
added theorem nat.floor_lt_iff
added theorem nat.floor_mono
added theorem nat.floor_of_nonpos
added theorem nat.floor_pos
added theorem nat.floor_zero
added theorem nat.le_ceil
added theorem nat.le_floor_iff
added theorem nat.le_floor_of_le
added theorem nat.le_of_ceil_le
added theorem nat.lt_ceil
added theorem nat.lt_floor_add_one
added theorem nat.lt_of_ceil_lt
added theorem nat.lt_of_lt_floor
added theorem nat.pos_of_floor_pos
added theorem nat.sub_one_lt_floor
deleted def nat_ceil
deleted theorem nat_ceil_add_nat
deleted theorem nat_ceil_coe
deleted theorem nat_ceil_eq_zero
deleted theorem nat_ceil_le
deleted theorem nat_ceil_lt_add_one
deleted theorem nat_ceil_mono
deleted theorem nat_ceil_zero
deleted def nat_floor
deleted theorem nat_floor_add_nat
deleted theorem nat_floor_coe
deleted theorem nat_floor_eq_zero_iff
deleted theorem nat_floor_le
deleted theorem nat_floor_lt_iff
deleted theorem nat_floor_mono
deleted theorem nat_floor_of_nonpos
deleted theorem nat_floor_pos
deleted theorem nat_floor_zero
deleted theorem pos_of_nat_floor_pos
deleted theorem sub_one_lt_floor
deleted theorem sub_one_lt_nat_floor