Commit 2022-11-30 10:44 2aa04f65

View on Github →

feat(algebra/order/to_interval_mod): lemmas about changing the base of the period (#17741) The lemmas have primed names because the unprimed names refer to the versions where one of the arguments is the period.

Estimated changes

Modified src/algebra/order/to_interval_mod.lean

added theorem to_Ico_div_add_right'

added theorem to_Ico_div_neg

added theorem to_Ico_div_sub'

added theorem to_Ico_mod_add_right'

added theorem to_Ico_mod_neg

added theorem to_Ico_mod_sub'

added theorem to_Ioc_div_add_right'

added theorem to_Ioc_div_neg

added theorem to_Ioc_div_sub'

added theorem to_Ioc_mod_add_right'

added theorem to_Ioc_mod_neg

added theorem to_Ioc_mod_sub'