Existence of irreducible factor of cyclotomic polynomial

Stream: Is there code for X?

[metakuntyyy]

Let p be prime, r be a natural number and let $\phi$ be the r-th cyclotomic polynomial over $\mathbb{F}_p$.
There exists an irreducible factor of degree $o_r(p)$ where $o_r(p)$ is the smallest natural number i such that $p^i=1 (\mod r)$

This means that $\phi$ divides $X^r-1$ in $\mathbb{F}_p[X]$

[metakuntyyy]

On second thought, is it https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.html#Polynomial.orderOf_root_cyclotomic_dvd

If so, how do I understand the proof?

[Kevin Buzzard]

Phi_r divides X^r-1 over Z, not just Z/p. Indeed the product of Phi_d over d dividing N is X^N-1.

[Kevin Buzzard]

To understand the proof, fire it up in VS Code and hover over everything. But why not just read a maths book proof and understand that instead?

[metakuntyyy]

Yes indeed, but while $\phi$ is irreducible over $\mathbb{Z}$ it is not necessarily irreducible over $\mathbb{F}_p$, however there exists an irreducible factor of degree $o_p(r)$.

I had quite the difficulty finding literature for this precise result.

[Johan Commelin]

Kevin Buzzard said:

To understand the proof, fire it up in VS Code and hover over everything. But why not just read a maths book proof and understand that instead?

I understand your second answer. But I really hope we won't need this fallback option in the near future.

[metakuntyyy]

I was speaking more of the line of that the theorems themselves lack any api/documentation on how to use them. I know that you can click in vscode and read the theorem. What I'd like to have is also an explanation on what the theorem does and how to use it. For example in Galois fields I had extensive troubles figuring out how to use them to show simple results. I think examples how to use the Theorems to do some simple calculations would be very helpful. For example if I define the Galois field GF(4) I'd like to construct all 4 elements and show that the product of non-zero,non-one elements are one. I'd also like to see what the concrete representation themselves is.

Sometimes it's particularly hard to understand the internal logic of a proof, especially when tactics like rfl and decide are used.

Yesterday I've spent looking at the api of Irreducible elements but I couldn't find a good theorem that would allow me to deduce that there exists a irreducible factor of degree $o_p(r)$. However I could find some literature https://www.math.rwth-aachen.de/homes/Max.Neunhoeffer/Teaching/ff/ffchap4.pdf that would be correct.

It appears that this result is not yet in mathlib, as such I'd like to formalise it. These are the steps I think are relevant:
$n$-th primitive roots exist for $\mathbb{F}_q$ if $\gcd(q,n)=1$. If $d=\gcd(q,n)$ then $\xi\in \mathbb{F}_{p^d}$ but not in any smaller subfield.
Then some more magic happens and then the proof concludes. I fail to see how this element is irreducible.

I must be missing some crucial theory. Here the existence of an irreducible element is constructed by taking a primitive root in a bigger field and saying that the smallest field that has this root is $\mathbb{F}_{q^d}$. This is a non-sequitur to me, I must be missing some theory.

I'd like to add to mathlib but without some directed guidance and a little bit of handholding I am completely lost and I fail to see the point in even trying, given how steep the learning curve is.

[Scott Carnahan]

I think you really want the fact that the multiplicative group of an order q finite field is cyclic of order q-1.