Commit 2023-01-17 10:21 a993e7ee

View on Github →

feat(algebra/order/to_interval_mod): more relations between to_Ixx_{mod/div} definitions (#17933) to_Ico_div and to_Ioc_div differ by at most 1, and the modulo versions differ by at most b. This also renames some lemmas that have the wrong name.

Estimated changes

Modified src/algebra/order/to_interval_mod.lean

deleted theorem mem_Ioo_mod_iff_eq_mod_zmultiples

added theorem mem_Ioo_mod_iff_ne_add_zsmul

added theorem mem_Ioo_mod_iff_ne_mod_zmultiples

deleted theorem mem_Ioo_mod_iff_sub_ne_zsmul

deleted theorem mem_Ioo_mod_iff_to_Ico_div_add_one_ne_to_Ioc_div

added theorem mem_Ioo_mod_iff_to_Ico_div_ne_to_Ioc_div_add_one

added theorem not_mem_Ioo_mod_iff_eq_add_zsmul

added theorem not_mem_Ioo_mod_iff_eq_mod_zmultiples

added theorem not_mem_Ioo_mod_iff_to_Ico_div_eq_to_Ioc_div_add_one

added theorem not_mem_Ioo_mod_iff_to_Ico_mod_add_period_eq_to_Ioc_mod

added theorem not_mem_Ioo_mod_iff_to_Ico_mod_eq_left

added theorem not_mem_Ioo_mod_iff_to_Ioc_eq_right

added theorem to_Ico_mod_le_to_Ioc_mod

added theorem to_Ioc_div_wcovby_to_Ico_div

added theorem to_Ioc_mod_le_to_Ico_mod_add

Modified src/topology/instances/add_circle.lean