Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-08 16:37 313fe11b

View on Github →

feat(algebra/floor): Split floor from archimedean file. (#1372)

  • feat(algebra/floor): Split floor from archimedean file.
  • feat({algebra,rat}/floor): move lemmas/defs from rat.floor to algebra.floor

Estimated changes

deleted def ceil
deleted theorem ceil_add_int
deleted theorem ceil_coe
deleted theorem ceil_le
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_coe
deleted theorem floor_eq_iff
deleted theorem floor_fract
deleted theorem floor_le
deleted theorem floor_lt
deleted theorem floor_mono
deleted theorem floor_nonneg
deleted theorem floor_one
deleted theorem floor_sub_int
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
deleted theorem le_ceil
deleted theorem le_floor
deleted theorem lt_ceil
deleted theorem lt_floor_add_one
deleted theorem lt_succ_floor
deleted theorem sub_one_lt_floor
added def ceil
added theorem ceil_add_int
added theorem ceil_coe
added theorem ceil_le
added theorem ceil_lt_add_one
added theorem ceil_mono
added theorem ceil_nonneg
added theorem ceil_pos
added theorem ceil_sub_int
added theorem ceil_zero
added def floor
added theorem floor_add_fract
added theorem floor_add_int
added theorem floor_coe
added theorem floor_eq_iff
added theorem floor_fract
added theorem floor_le
added theorem floor_lt
added theorem floor_mono
added theorem floor_nonneg
added theorem floor_one
added theorem floor_ring_unique
added theorem floor_sub_int
added theorem floor_zero
added def fract
added theorem fract_add
added theorem fract_add_floor
added theorem fract_coe
added theorem fract_eq_fract
added theorem fract_eq_iff
added theorem fract_floor
added theorem fract_fract
added theorem fract_lt_one
added theorem fract_mul_nat
added theorem fract_nonneg
added theorem fract_zero
added theorem le_ceil
added theorem le_floor
added theorem le_nat_ceil
added theorem lt_ceil
added theorem lt_floor_add_one
added theorem lt_nat_ceil
added theorem lt_succ_floor
added def nat_ceil
added theorem nat_ceil_add_nat
added theorem nat_ceil_coe
added theorem nat_ceil_le
added theorem nat_ceil_lt_add_one
added theorem nat_ceil_mono
added theorem nat_ceil_zero
added theorem sub_one_lt_floor
deleted def rat.ceil
deleted theorem rat.ceil_add_int
deleted theorem rat.ceil_coe
deleted theorem rat.ceil_le
deleted theorem rat.ceil_mono
deleted theorem rat.ceil_sub_int
deleted def rat.floor
deleted theorem rat.floor_add_int
deleted theorem rat.floor_coe
deleted theorem rat.floor_def
deleted theorem rat.floor_le
deleted theorem rat.floor_lt
deleted theorem rat.floor_mono
deleted theorem rat.floor_sub_int
deleted theorem rat.le_ceil
deleted theorem rat.le_floor
deleted theorem rat.le_nat_ceil
deleted theorem rat.lt_nat_ceil
deleted theorem rat.lt_succ_floor
deleted def rat.nat_ceil
deleted theorem rat.nat_ceil_add_nat
deleted theorem rat.nat_ceil_coe
deleted theorem rat.nat_ceil_le
deleted theorem rat.nat_ceil_lt_add_one
deleted theorem rat.nat_ceil_mono
deleted theorem rat.nat_ceil_zero