[Merged by Bors] - fix: add missing _root_#3630
Closed
eric-wieser wants to merge 10 commits intomasterfrom
Closed
Conversation
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead.
2 tasks
| #align equiv.mul_left₀_apply Equiv.mulLeft₀_apply | ||
|
|
||
| theorem mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * ·) a : G → G) := | ||
| theorem _root_.mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * ·) a : G → G) := |
Contributor
There was a problem hiding this comment.
Should this also be mul_left? But maybe it's better to keep this pr focused tightly.
Member
Author
|
@Parcly-Taxel, your latest commit is great, but I don't think it belongs in this PR. Please revert it and make a new PR with that change. |
Collaborator
I needed to do it to get the full list of possible misalignments: #!/usr/bin/env python3
with open("matches", 'r') as f:
for l in f:
fn, _, ln = l.strip().partition(":")
try:
name3, name4 = ln.split(" ")[1:3]
if name3.count(".") < name4.count("."):
print(fn, "->", name3, "/", name4)
except ValueError:
print("*****", l) |
709846d to
7d7d470
Compare
Member
Author
All the more reason to do this in a separate PR and get it merged first! |
…-community/mathlib4 into eric-wieser/fix-root-screwups
bors bot
pushed a commit
that referenced
this pull request
Apr 25, 2023
This PR fixes two things: * Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks. * **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
Ruben-VandeVelde
approved these changes
Apr 25, 2023
Member
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Apr 25, 2023
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
_root__root_
kim-em
pushed a commit
that referenced
this pull request
May 10, 2023
This PR fixes two things: * Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks. * **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
kim-em
pushed a commit
that referenced
this pull request
May 10, 2023
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 10, 2023
This PR fixes two things: * Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks. * **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
hrmacbeth
pushed a commit
that referenced
this pull request
May 10, 2023
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
hrmacbeth
pushed a commit
that referenced
this pull request
May 11, 2023
This PR fixes two things: * Most `align` statements for definitions and theorems and instances that are separated by two newlines from the relevant declaration (`s/\n\n#align/\n#align`). This is often seen in the mathport output after ending `calc` blocks. * **All** remaining more-than-one-line `#align` statements. (This was needed for a script I wrote for #3630.)
hrmacbeth
pushed a commit
that referenced
this pull request
May 11, 2023
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates. If your `#align` statement complains the def doesn't exist, **don't change the #align**; work out why it doesn't exist instead. Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Mathport doesn't understand this, and apparently nor do many of the humans fixing the errors it creates.
If your
#alignstatement complains the def doesn't exist, don't change the #align; work out why it doesn't exist instead.