doc(misc): update two theorem names#36220
doc(misc): update two theorem names#36220harahu wants to merge 1 commit intoleanprover-community:masterfrom
Conversation
PR summary 9d0ea7dd98Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
| title: Bézout's theorem | ||
|
|
||
| Q1543149: | ||
| title: Sokhatsky–Weierstrass theorem |
There was a problem hiding this comment.
In the 1000 theorems repo and on the Wikipedia list of theorems, the name is "Sokhatsky–Weierstrass theorem". Why should it change here?
There was a problem hiding this comment.
If you click the link in the Wikipedia list of theorems, you'll find that the actual article for that theorem is named: Sokhotski–Plemelj theorem.
That's my reason for suggesting it.
There was a problem hiding this comment.
The talk page of that article gives an explanation of why the name we're currently using is a misunderstanding.
There was a problem hiding this comment.
Since mathlib's file here is intended to mirror https://1000-plus.github.io/, I feel like the first step here would be to land your correction in that project (and perhaps also https://en.wikipedia.org/wiki/List_of_theorems ).
There was a problem hiding this comment.
I don't mind updating the 1000+ repo as well, and can commit to doing that. But I don't intend to become a Wikipedia contributor, so I won't be fixing the list, unfortunately.
I also don't know that the order of the fixes matters: The name is just aesthetics AFAIK, what needs to mirror 1000+ is the QID, which remains untouched.
There was a problem hiding this comment.
4 participants
Uh oh!
There was an error while loading. Please reload this page.