-
Notifications
You must be signed in to change notification settings - Fork 88
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
Move 'monoid of endomorphisms' subsection from my mathbox to Main. #4249
base: develop
Are you sure you want to change the base?
Conversation
…orten a few proofs.
Do we really need a definition According our convention "New definitions infrequent",
I don't see any of these advantages (yet). Therefore, this PR must be rejected (sorry). I remember that I proposed to move some definitions from my Mathbox to main some time ago (see, for example, #1389) which was rejected for this reason... |
Yes, https://us.metamath.org/mpeuni/df-bj-end.html is a worthy addition to set.mm. This is an important notion, which a quick internet or library search will suffice to confirm. I move it to Main with this PR as requested by @tirix @zwang123 and @langgerard in #4242 (comment) and #4242 (comment). Actually, had this already been in Main before #4242, @zwang123 would have probably spent less time reproving some results, and would have used that definition instead. I think the comparison of the statements
and
speaks for itself. In particular, the first statement is more readily understandable to readers, without having to know about the implementation details exposed in the second. |
With the same arguments, my definition of non-unitary rings (and maybe others) can also be moved to main, which was rejected some time ago. So can I move df-rng0 and related theorems also to main (so #1389 will be solved, being "on hold" for more than 4 years)? I want to hear the opinion of @david-a-wheeler and @digama0 at least. |
1 : In my personal opinion, the position of BJ is basically correct, and he should be allowed to move his "monoid of endomorphisms subsection " to the main part of set.mm. |
The same arguments? When that move to Main was proposed, had that move been requested by three other contributors too? Had another contributor started working independently on the same topic and accidentally duplicated the work, too? More generally, this really shouldn't become a bargaining of the form: "you accept my definition, I accept yours". As for df-rng0 specifically, the first reply to your issue #1389 was by me and it was an approval to move df-rng0 to Main as df-rng. I haven't changed on that point. So to be explicit: I do approve the moving of df-rng0 to Main (relabeled to df-rng). I reiterated my approval in #1389 (comment) and then I gave ideas of developments in #1389 (comment). That's the least I could do since I drew attention to them in https://groups.google.com/g/metamath/c/XKl7K0qx4uc/m/WOghVowaDgAJ and in #866 (comment). In the case of endomorphisms, I also drew attention to them in #3782 (comment), in which I used them to answer a basic question that was asked by contributors. This is actually the reason why I felt I had to provide the associated definition in my mathbox. Recently, three contributors requested that I move it to Main, which I accepted, and here we are. |
Sorry for nosing in, but maybe someone (say, zwang123) could prove prove a few theorems using benjub's definitions, and that would trigger the formal criteria for moving material from his mathbox? I think we have been routinely moving stuff into main if it's required by other contributors. That way we can rely on a strict procedure instead of judging whether some results are better than others. |
ovigg $p |- ( ( A e. V /\ B e. W /\ C e. X ) -> | ||
( ps -> ( A F B ) = C ) ) $= | ||
ovigg $p |- | ||
( ( A e. V /\ B e. W /\ C e. X ) -> ( ps -> ( A F B ) = C ) ) $= |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I find some of these reformattings a bit dubious. I'm very much not a fan of right alignment, and would prefer we used a consistent formatting style in the library.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I can revert that. I thought the rule of thumb was to break line at highest possible token (in the sense of "oldest in the syntax tree), and I would actually break these at $p
if not for formatting problems arising from that choice.
Consistency is indeed paramount. Actually, I wouldn't mind having an automatic "dumb" line-wrap as for proofs and comments.
I have no substantive comments, but I agree with @savask that when in doubt we should apply our procedures. If there is consensus that it should be moved to main then I am not opposed, but if there is any doubt or debate then probably it would be better to wait until some other mechanism kicks in, like usage by multiple contributors. |
I think this is exactly the way which should be followed, because it is completely in accordance with our conventions. |
Move 'monoid of endomorphisms' subsection from my mathbox to Main.
Shorten a few proofs.