Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-15 01:06 be91f696

View on Github →

chore(algebra/floor): general golf (#9716) This cleans the file in depth:

  • kill some simp
  • use available dot notation on ≤
  • remove the by ... ; ... (there's one left that #9715) takes care of
  • group definition and notation of int.floor,int.ceil and int.fract
  • move int.preimage_... lemmas with the rest of the ℤ stuff
  • homogeneize variable names

Estimated changes

modified def int.ceil
modified theorem int.ceil_add_int
modified theorem int.ceil_coe
modified theorem int.ceil_eq_iff
modified theorem int.ceil_eq_on_Ioc'
modified theorem int.ceil_eq_on_Ioc
modified theorem int.ceil_le
modified theorem int.ceil_le_floor_add_one
modified theorem int.ceil_lt_add_one
modified theorem int.ceil_mono
modified theorem int.ceil_nonneg
modified theorem int.ceil_pos
modified theorem int.ceil_sub_int
modified theorem int.ceil_zero
deleted theorem int.floor_add
modified theorem int.floor_add_fract
modified theorem int.floor_add_int
modified theorem int.floor_add_nat
modified theorem int.floor_coe
modified theorem int.floor_eq_iff
modified theorem int.floor_eq_on_Ico'
modified theorem int.floor_eq_on_Ico
modified theorem int.floor_fract
modified theorem int.floor_int_add
modified theorem int.floor_le
modified theorem int.floor_lt
modified theorem int.floor_lt_ceil_of_lt
modified theorem int.floor_mono
added theorem int.floor_nat_add
modified theorem int.floor_nonneg
modified theorem int.floor_one
modified theorem int.floor_sub_int
modified theorem int.floor_sub_nat
modified theorem int.floor_zero
modified def int.fract
modified theorem int.fract_add
modified theorem int.fract_add_floor
modified theorem int.fract_eq_fract
modified theorem int.fract_eq_iff
modified theorem int.fract_floor
modified theorem int.fract_fract
modified theorem int.fract_lt_one
modified theorem int.fract_mul_nat
modified theorem int.fract_nonneg
modified theorem int.fract_zero
modified theorem int.le_ceil
modified theorem int.le_floor
modified theorem int.lt_ceil
modified theorem int.lt_floor_add_one
modified theorem int.lt_succ_floor
modified theorem int.preimage_Icc
modified theorem int.preimage_Ici
modified theorem int.preimage_Ico
modified theorem int.preimage_Iic
modified theorem int.preimage_Iio
modified theorem int.preimage_Ioc
modified theorem int.preimage_Ioi
modified theorem int.preimage_Ioo
modified theorem int.sub_one_lt_floor
modified theorem nat.ceil_add_nat
modified theorem nat.ceil_coe
modified theorem nat.ceil_eq_zero
modified theorem nat.ceil_le
modified theorem nat.ceil_mono
modified theorem nat.ceil_zero
modified theorem nat.floor_add_nat
modified theorem nat.floor_coe
modified theorem nat.floor_lt_iff
modified theorem nat.floor_mono
modified theorem nat.floor_zero
modified theorem nat.le_ceil
modified theorem nat.le_floor_iff
modified theorem nat.le_of_ceil_le
modified theorem nat.lt_ceil
modified theorem nat.lt_of_ceil_lt
modified theorem nat.sub_one_lt_floor