-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: Rename mul
-div
cancellation lemmas
#11530
Conversation
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |---------------------|-------------------------|-------------------------| | `(a * b) / a = b` | `mul_div_eq_right₀` | `mul_div_cancel_left` | | | `mul_div_eq_right` | `mul_div_cancel'''` | | | `add_sub_eq_right` | `add_sub_cancel'` | | `(a * b) / b = a` | `mul_div_eq_left₀` | `mul_div_cancel` | | | `mul_div_eq_left` | `mul_div_cancel''` | | | `add_sub_eq_left` | `add_sub_cancel` | | `a / (a * b) = b⁻¹` | `div_mul_eq_inv_right₀` | roughly `div_mul_right` | | | `div_mul_eq_inv_right` | `div_mul_cancel''` | | | `sub_add_eq_neg_right` | `sub_add_cancel'` | | `a / (a * b) = a⁻¹` | `div_mul_eq_inv_left₀` | roughly `div_mul_left` | | | `div_mul_eq_inv_left` | `div_mul_cancel'''` | | | `sub_add_eq_neg_left` | `sub_add_cancel''` | | `a * (b / a) = b` | `mul_div_cancel₀` | `mul_div_cancel'` | | | `mul_div_cancel` | `mul_div_cancel'_right` | | | `add_sub_cancel` | `add_sub_cancel'_right` | | `(a / b) * b = a` | `div_mul_cancel₀` | `div_mul_cancel` | | | `div_mul_cancel` | `div_mul_cancel'` | | | `sub_add_cancel` | `sub_add_cancel` |
For these kinds of basic lemma renames, it might be good to make a Zulip thread with the suggested renames, and only do it if nobody makes a major objection for 1-2 days. That said, this is definitely an improvement over all the primed lemmas. However, it's a bit unfortunate that in the new naming scheme the |
Second Zulip thread for more visibility. I'm happy to merge this in ~24 hours if there is no serious criticism. |
I think the rename I suggested is popular. If you change the names to that naming scheme, then I'll merge/delegate this. |
LGTM. I didn't have time yesterday to look at this again, so hopefully there are not conflicts. bors merge (let's try, but I'm not too hopeful) |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
Build failed:
|
Build failed (retrying...): |
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
Pull request successfully merged into master. Build succeeded: |
mul
-div
cancellation lemmasmul
-div
cancellation lemmas
This is fallout from #11530. Somehow CI didn't catch that.
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess. This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the `GroupWithZero` lemma name, the `Group` lemma, the `AddGroup` lemma name). | Statement | New name | Old name | |
We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in `checkYaml` only imports `Mathlib`. This PR changes it to also import `Archive`. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from `lake build Archive` (see #11612). Co-authored-by: Enrico Borba <enricozb@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
CI didn't catch the fallout from #11530 because we forgot to pipe the errors coming from `lake build Archive` and `lake build Counterexamples` back to the logs. This PR makes sure that happens.
Lemma names around cancellation of multiplication and division are a mess.
This PR renames a handful of them according to the following table (each big row contains the multiplicative statement, then the three rows contain the
GroupWithZero
lemma name, theGroup
lemma, theAddGroup
lemma name).(a * b) / a = b
mul_div_cancel_left₀
mul_div_cancel_left
mul_div_cancel_left
mul_div_cancel'''
add_sub_cancel_left
add_sub_cancel'
(a * b) / b = a
mul_div_cancel_right₀
mul_div_cancel
mul_div_cancel_right
mul_div_cancel''
add_sub_cancel_right
add_sub_cancel
a / (a * b) = b⁻¹
div_mul_cancel_left₀
div_mul_right
(roughly)div_mul_cancel_left
div_mul_cancel''
sub_add_cancel_left
sub_add_cancel'
b / (a * b) = a⁻¹
div_mul_cancel_right₀
div_mul_left
(roughly)div_mul_cancel_right
div_mul_cancel'''
sub_add_cancel_right
sub_add_cancel''
a * (b / a) = b
mul_div_cancel₀
mul_div_cancel'
mul_div_cancel
mul_div_cancel'_right
add_sub_cancel
add_sub_cancel'_right
(a / b) * b = a
div_mul_cancel₀
div_mul_cancel
div_mul_cancel
div_mul_cancel'
sub_add_cancel
sub_add_cancel