Accidentally brought a new file into my PR

Stream: new members

[Sebastian Monnet]

While trying to fix another issue, I clicked the "pull" option on my PR, #11973, which added the file number_theory/cyclotomic/zeta. This file is not mine, and I don't understand how I added it to the PR. Is there a way I can remove it, or do I have to start a new PR?

[Riccardo Brasca]

This file existed at some point and then we changed its name. You can just merge master (to be sure you're up-to-date), and remove it, commit and push.

[Riccardo Brasca]

And a tip: if you write #11973 (without the `) you automatically get a link to the PR

[Sebastian Monnet]

Thank you, those are both very helpful tips!