Is this special case of Rational Root Theorem needed?

Stream: mathlib4

[Ilmārs Cīrulis]

It's the specialization of the theorem for standard integers and rational numbers.
It's here: #new members > How to use Rational Root Theorem? @ 💬 (thanks to Ruben Van de Velde for his help)

1) Is it needed in Mathlib? (I would argue that yes, because general case was too general for me. :sweat_smile: )
2) Where to put it, if answer to 1) is positive.

Anyway, reading guidelines as the proof must be put in the shape (for example, naming almost all theorems/lemmas aux is probably acceptable only in draft). It will be good to learn the guidelines in any case.

[Michał Mrugała]

It's a generally good idea to name everything in accordance with the naming convention as you write it. For people like @Yaël Dillies it's borderline automatic at this point. (I say as I name my lemmas aux and gigaOmegaDiagram)

[Ilmārs Cīrulis]

Did my best to rewrite it in accordance to the guidelines. :)

[Ilmārs Cīrulis]

I see no objections. :sweat_smile:

So... where in the Mathlib could the file go? :thinking:

[Ilmārs Cīrulis]

Finally all checks are green: #24172 :partying_face:

(I made PR etc. It was fun and, if something, I can always close it.)