[Merged by Bors] - feat(algebra/order/to_interval_mod): symmetric variants of lemmas #18942
Conversation
eric-wieser
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
| @[simp] lemma to_Ioc_div_sub' (a b : α) : to_Ioc_div hp (a - p) b = to_Ioc_div hp a b + 1 := | ||
| by simpa only [one_zsmul] using to_Ioc_div_sub_zsmul' hp a b 1 | ||
|
|
||
| lemma to_Ico_div_sub_eq (a b c : α) : to_Ico_div hp a (b - c) = to_Ico_div hp (a + c) b := |
There was a problem hiding this comment.
I'm not super happy with this new name (previously to_Ico_div_sub'). Some other options are:
to_Ico_div_sub''(if in doubt, add more primes)to_Ico_div_sub_eq_to_Ico_div_add(perhaps too long?)
There was a problem hiding this comment.
I think to_Ico_div_sub_eq_to_Ico_div_add because it's not so clear which should be the LHS and which should be the RHS, so having both to_Ico_div_sub and to_Ico_div_add with the name will with the search. But yeah I agree it's annoyingly long (but gets better with CamelCase).
There was a problem hiding this comment.
Done, this scheme seems to work nicely for the other clashes too
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
|
bors merge @YaelDillies, I can address any remaining missing lemmas in a follow-up if you add further comments here. |
github-actions
bot
added
the
ready-to-merge
…8942) 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.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
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_addto_Ioc_div_sub'→to_Ioc_div_sub_eq_to_Ioc_div_addto_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_subto_Ioc_mod_sub'→to_Ioc_mod_sub_eq_subto_Ico_mod_add_right'→to_Ico_mod_add_right_eq_addto_Ioc_mod_add_right'→to_Ioc_mod_add_right_eq_addThe statement of
to_Ioc_div_zsmul_addis commuted to be consistent with the lemmas around it; presumably it was a copy-and-paste error.