Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-01 23:12 b2d7b50d

View on Github →

chore(algebra/order/to_interval_mod): Reorder arguments (#18908) The current argument order to to_Ixx_mod is a bit poor: In to_Ico a hb x, a and x play a similar role while b is completely separate. This PR changes this to to_Ico hp a b, where the translation is as follows:

  • mem_Ioo_mod a p b → mem_Ioo_mod p a b (this is more consistent with int.modeq p a b)
  • to_Ico_div a hp b → to_Ico_div hp a b
  • to_Ioc_div a hp b → to_Ioc_div hp a b
  • to_Ico_mod a hp b → to_Ico_mod hp a b
  • to_Ioc_mod a hp b → to_Ioc_mod hp a b While it might be tempting to orderto_Ico_div hp a b as to_Ico_div b a hp to match the order of the morally equivalent (b - a) / p + a, we opt for the simpler convention of being consistent with mem_Ioo_mod, as in downstream files we also find it convenient to have b as the last argument. Generally speaking, the variables have been renamed to
  • a → a (the left end)
  • b → p (the period)
  • x → b (the interval length)
  • y → c (additional argument similar to the left end and interval length)
  • z → n (the euclidean dividend) Proofs are golfed slightly. The only lemma statements that changed are to_Ico_div_eq_of_sub_zsmul_mem_Ico/to_Ioc_div_eq_of_sub_zsmul_mem_Ioc that now state to_Ico_div hp a b = n rather than n = to_Ico_div hp a b (they were always used in this new direction).

Estimated changes

modified theorem Union_Icc_add_zsmul
modified theorem Union_Icc_zsmul
modified theorem Union_Ico_add_zsmul
modified theorem Union_Ico_zsmul
modified theorem Union_Ioc_add_zsmul
modified theorem Union_Ioc_zsmul
modified theorem left_le_to_Ico_mod
modified theorem left_lt_to_Ioc_mod
modified def mem_Ioo_mod
modified theorem self_sub_to_Ico_div_zsmul
modified theorem self_sub_to_Ico_mod
modified theorem self_sub_to_Ioc_div_zsmul
modified theorem self_sub_to_Ioc_mod
modified def to_Ico_div
modified theorem to_Ico_div_add_left
modified theorem to_Ico_div_add_right'
modified theorem to_Ico_div_add_right
modified theorem to_Ico_div_add_zsmul
modified theorem to_Ico_div_apply_left
modified theorem to_Ico_div_apply_right
modified theorem to_Ico_div_eq_floor
modified theorem to_Ico_div_neg
modified theorem to_Ico_div_sub'
modified theorem to_Ico_div_sub
modified theorem to_Ico_div_sub_zsmul
modified theorem to_Ico_div_zero_one
modified theorem to_Ico_div_zsmul_add
modified theorem to_Ico_div_zsmul_sub_self
modified def to_Ico_mod
modified theorem to_Ico_mod_add_left
modified theorem to_Ico_mod_add_right'
modified theorem to_Ico_mod_add_right
modified theorem to_Ico_mod_add_zsmul
modified theorem to_Ico_mod_apply_left
modified theorem to_Ico_mod_apply_right
modified theorem to_Ico_mod_eq_add_fract_mul
modified theorem to_Ico_mod_eq_fract_mul
modified theorem to_Ico_mod_eq_iff
modified theorem to_Ico_mod_eq_self
modified theorem to_Ico_mod_eq_to_Ico_mod
modified theorem to_Ico_mod_le_to_Ioc_mod
modified theorem to_Ico_mod_lt_right
modified theorem to_Ico_mod_mem_Ico'
modified theorem to_Ico_mod_mem_Ico
modified theorem to_Ico_mod_neg
modified theorem to_Ico_mod_periodic
modified theorem to_Ico_mod_sub'
modified theorem to_Ico_mod_sub
modified theorem to_Ico_mod_sub_self
modified theorem to_Ico_mod_sub_zsmul
modified theorem to_Ico_mod_to_Ico_mod
modified theorem to_Ico_mod_to_Ioc_mod
modified theorem to_Ico_mod_zero_one
modified theorem to_Ico_mod_zsmul_add
modified def to_Ioc_div
modified theorem to_Ioc_div_add_left
modified theorem to_Ioc_div_add_right'
modified theorem to_Ioc_div_add_right
modified theorem to_Ioc_div_add_zsmul
modified theorem to_Ioc_div_apply_left
modified theorem to_Ioc_div_apply_right
modified theorem to_Ioc_div_eq_neg_floor
modified theorem to_Ioc_div_neg
modified theorem to_Ioc_div_sub'
modified theorem to_Ioc_div_sub
modified theorem to_Ioc_div_sub_zsmul
modified theorem to_Ioc_div_zsmul_add
modified theorem to_Ioc_div_zsmul_sub_self
modified def to_Ioc_mod
modified theorem to_Ioc_mod_add_left
modified theorem to_Ioc_mod_add_right'
modified theorem to_Ioc_mod_add_right
modified theorem to_Ioc_mod_add_zsmul
modified theorem to_Ioc_mod_apply_left
modified theorem to_Ioc_mod_apply_right
modified theorem to_Ioc_mod_eq_iff
modified theorem to_Ioc_mod_eq_self
modified theorem to_Ioc_mod_eq_sub_fract_mul
modified theorem to_Ioc_mod_eq_to_Ioc_mod
modified theorem to_Ioc_mod_le_right
modified theorem to_Ioc_mod_mem_Ioc
modified theorem to_Ioc_mod_neg
modified theorem to_Ioc_mod_periodic
modified theorem to_Ioc_mod_sub'
modified theorem to_Ioc_mod_sub
modified theorem to_Ioc_mod_sub_self
modified theorem to_Ioc_mod_sub_zsmul
modified theorem to_Ioc_mod_to_Ico_mod
modified theorem to_Ioc_mod_to_Ioc_mod
modified theorem to_Ioc_mod_zsmul_add
modified theorem real.angle.coe_to_Ico_mod
modified theorem real.angle.coe_to_Ioc_mod
modified theorem real.angle.to_real_coe
modified def add_circle.equiv_Ico
modified def add_circle.equiv_Ioc
modified theorem continuous_at_to_Ico_mod
modified theorem continuous_at_to_Ioc_mod
modified theorem continuous_left_to_Ioc_mod
modified theorem continuous_right_to_Ico_mod