[Merged by Bors] - chore(ring_theory/polynomial/cyclotomic): fix namespacing

[ericrbg]

@riccardobrasca told me I got it wrong, so I fixed it :)

---

[riccardobrasca]

I always do mistakes with the name convention, so I will let someone else judge this, but those I am not sure about are polynomial.coprime_of_root_cyclotomic, polynomial.order_of_root_cyclotomic_dvd, polynomial.order_of_root_cyclotomic and polynomial.minpoly_primitive_root_dvd_cyclotomic .

Note that even if they concerns roots of unity in any field, it's better to have them here, since they need cyclotomic polyomials, over ℤ, whose definition uses the complex numbers.

[ericrbg]

Thanks, I switched it to the shorter named and changed order_of_root_cyclotomic to order_of_root_cyclotomic_eq. For a separate PR, Riccardo, is there any specific reason that the last few results are specialized to ℤ? Is it just because everything is a ℤ-algebra, so it doesn't particularly matter? I'm glad to put in the effort generalising if not.

[jcommelin]

Thanks 🎉

bors merge

[jcommelin]

Thanks, I switched it to the shorter named and changed order_of_root_cyclotomic to order_of_root_cyclotomic_eq. For a separate PR, Riccardo, is there any specific reason that the last few results are specialized to ℤ? Is it just because everything is a ℤ-algebra, so it doesn't particularly matter? I'm glad to put in the effort generalising if not.

@ericrbg The statement cyclotomic n R = minpoly R \mu is not true for general R. So the statement would become more complicated. I think it's fine to keep \Z there.

[bors]

Pull request successfully merged into master.

Build succeeded:

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

[riccardobrasca]

As Johan said, some statements are not true in general, and I am not sure they are easy to generalize.