[Merged by Bors] - chore(ring_theory/polynomial/cyclotomic): golf+remove nontrivial

[ericrbg]

---

[riccardobrasca]

Very nice, thank you!

[riccardobrasca]

Since you are modifying the file ring_theory.polynomial.cyclotomic.lean can you check the name of the last lemmas? There is at least cyclotomic.irreducible that should definitely be polynomial.cyclotomic.irreducible (I think I closed the namespace and then forget about it).

[ericrbg]

I did that and then got a little carried away ­— sorry!

[semorrison]

Looks good to me. (An aside: the description of the easy tag is "<20 of review time". I agree this one is easy, but not short enough to really be easy.)

bors merge

[ericrbg]

Sorry Scott, forgot to remove it after the second commit! The first one was like 7 lines :)

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[riccardobrasca]

Sorry to bother you again, but I think you changed the name of too many lemmas: polynomial.cyclotomic.irreducible and polynomial.cyclotomic_eq_minpoly are perfect now, but minpoly_primitive_root_dvd_cyclotomic I think it should not have polynomial.. I am not sure about the other ones...

[ericrbg]

#9116, sorry I messed it up! I went through and all the other namespaces seemed okay