Open Polynomials PR

Stream: new members

[Gareth Ma]

I have an open PR on some simple polynomial lemmas here, I found them useful while working on some proofs. If someone could review it that would be great :)

[Bolton Bailey]

Welcome to mathlib contribution! If you want someone to review the PR, you should put the awaiting-review label on it

[Gareth Ma]

Thanks, just curious why isn't this added automatically :D

[Bolton Bailey]

Contributors often want to continue work on their PRs, even after they are passing CI. I think its technically supposed to be the case that every PR is labeled either WIP awaiting-review or awaiting-author. You can read more here.

[Gareth Ma]

Ah interesting. I was thinking that if someone wants to keep working on a PR before being reviewed, they can mark it as draft. But I guess that turns off CI

[Bolton Bailey]

No actually I think ci works either way, it’s just redundant as a system

[Bolton Bailey]

In fact I have had people review draft prs of mine before that weren’t marked in any way, the system is just a free for all

[Yaël Dillies]

... or awaiting-zulip