Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-06 13:10 4c8f86bd

View on Github →

feat(algebra/order/to_interval_mod): symmetric variants of lemmas (#18942) These lemmas are about expressions in the second instead of third arguments of the I{co,oc}_{mod,div} functions. Some existing lemmas clashed with these new lemmas; they have been renamed as follows:

to_Ico_div_sub' → to_Ico_div_sub_eq_to_Ico_div_add
to_Ioc_div_sub' → to_Ioc_div_sub_eq_to_Ioc_div_add
to_Ico_div_add_right' → to_Ico_div_sub_eq_to_Ico_div_add' (and reversed)
to_Ioc_div_add_right' → to_Ioc_div_sub_eq_to_Ioc_div_add' (and reversed)
to_Ico_mod_sub' → to_Ico_mod_sub_eq_sub
to_Ioc_mod_sub' → to_Ioc_mod_sub_eq_sub
to_Ico_mod_add_right' → to_Ico_mod_add_right_eq_add
to_Ioc_mod_add_right' → to_Ioc_mod_add_right_eq_add The statement of to_Ioc_div_zsmul_add is commuted to be consistent with the lemmas around it; presumably it was a copy-and-paste error.

Estimated changes

Modified src/algebra/order/to_interval_mod.lean

added theorem to_Ico_div_add_left'

modified theorem to_Ico_div_add_right'

added theorem to_Ico_div_add_zsmul'

added theorem to_Ico_div_neg'

modified theorem to_Ico_div_sub'

added theorem to_Ico_div_sub_eq_to_Ico_div_add'

added theorem to_Ico_div_sub_eq_to_Ico_div_add

added theorem to_Ico_div_sub_zsmul'

added theorem to_Ico_mod_add_left'

modified theorem to_Ico_mod_add_right'

added theorem to_Ico_mod_add_right_eq_add

added theorem to_Ico_mod_add_zsmul'

added theorem to_Ico_mod_neg'

modified theorem to_Ico_mod_sub'

added theorem to_Ico_mod_sub_eq_sub

added theorem to_Ico_mod_sub_zsmul'

added theorem to_Ico_mod_zsmul_add'

added theorem to_Ioc_div_add_left'

modified theorem to_Ioc_div_add_right'

added theorem to_Ioc_div_add_zsmul'

added theorem to_Ioc_div_neg'

modified theorem to_Ioc_div_sub'

added theorem to_Ioc_div_sub_eq_to_Ioc_div_add'

added theorem to_Ioc_div_sub_eq_to_Ioc_div_add

added theorem to_Ioc_div_sub_zsmul'

added theorem to_Ioc_mod_add_left'

modified theorem to_Ioc_mod_add_right'

added theorem to_Ioc_mod_add_right_eq_add

added theorem to_Ioc_mod_add_zsmul'

added theorem to_Ioc_mod_neg'

modified theorem to_Ioc_mod_sub'

added theorem to_Ioc_mod_sub_eq_sub

added theorem to_Ioc_mod_sub_zsmul'

added theorem to_Ioc_mod_zsmul_add'