## Stream: Is there code for X?

### Topic: Factorization of Polynomials over Finite Fields

#### Tobias Rothmann (Jul 07 2023 at 19:56):

Hi,
I am trying to factorize polynomials over a finite field Fp (p is prime) into irreducible parts.
I am aware of the Berlekamp-Zassenhaus formalization, which covers integer polynomials, real polynomials, and square-free polynomials over finite fields, but I couldn't find a formalization for non-square-free polynomials over finite fields.
Additionally, there seems to be no general formalization for an algorithm that separates a polynomial over a finite field into square-free parts, the Yun algorithm works only on a Field with characteristic 0, which doesn't hold for Fp (where char(Fp)=p).
Although the mathematical literature commonly refers to the conversion into square-free parts as "easily done", I find the formalization of such algorithms (namely the "Square-free factorization" algorithm and the "Elimination of Repeated Factors" algorithm) quite time-intensive, and hence would greatly appreciate any help :)

Side note:
If you know how to compute all roots (in the sense of x for \<phi>(x) = 0) of a polynomial over a finite field, that would also solve the problem for me :)

#### Manuel Eberl (Jul 10 2023 at 10:38):

Maybe try asking René Thiemann by email. He might know, but I don't think he reads Zulip much. I do think he's on holiday right now though, so you might not get an answer that quickly.

#### Tobias Rothmann (Jul 12 2023 at 08:52):

Thanks for the hint, I'll contact him :)

#### Yong Kiam (Sep 28 2023 at 04:22):

(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)

#### Manuel Eberl (Sep 29 2023 at 11:28):

I think so, too, but you need to do a square free factorisation first

#### Tobias Rothmann (Sep 29 2023 at 13:57):

Yong Kiam said:

(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)

Hi thanks for the answer! :)
As Manuel said, I'm looking for "non square-free" factorization and the first line you're referring to says "square-free polynomial", right?

The Cantor–Zassenhaus algorithm takes as input a square-free polynomial

#### Emin Karayel (Sep 29 2023 at 14:12):

The trick to check whether a polynomial is square-free is to compute the gcd of it with its formal derivative.

#### Emin Karayel (Sep 29 2023 at 14:13):

E.g. if f has a square factor g then g will divide both f and f'.

#### Emin Karayel (Sep 29 2023 at 14:14):

I'm not sure whether you're using HOL-Algebra (I had defined formal polynomial derivates for them "https://www.isa-afp.org/theories/finite_fields/#Formal_Polynomial_Derivatives" )

#### Emin Karayel (Sep 29 2023 at 14:14):

There is also a library for formal derivatives in HOL-Computational_Algebra (if you're using the type-based approach)

#### Emin Karayel (Sep 29 2023 at 14:15):

It's called pderiv (defined in "https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html")

#### Emin Karayel (Sep 29 2023 at 14:27):

By repeatedly dividing by gcd(f,f') the polynomial can be split into a product of square-free polynomials.

#### Tobias Rothmann (Sep 29 2023 at 14:39):

Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from @Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).

#### Emin Karayel (Sep 29 2023 at 14:49):

Tobias Rothmann said:

Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).

Sounds good. Let me know if it works - and nice project btw. :)

#### Tobias Rothmann (Sep 29 2023 at 14:54):

Emin Karayel said:

Tobias Rothmann said:

Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).

Sounds good. Let me know if it works - and nice project btw. :)

Sure! And thanks a lot :)

#### Yong Kiam (Oct 02 2023 at 01:04):

Tobias Rothmann said:

Yong Kiam said:

(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)

Hi thanks for the answer! :)
As Manuel said, I'm looking for "non square-free" factorization and the first line you're referring to says "square-free polynomial", right?

The Cantor–Zassenhaus algorithm takes as input a square-free polynomial

ah sorry I hadn't checked the Zulip for a bit, I should have quoted this part of the Wikipedia sentence, which is what @Emin Karayel said

(algorithms exist for efficiently factoring arbitrary polynomials into a product of polynomials satisfying these conditions, for instance, f ( x ) / gcd ( f ( x ) , f ′ ( x ) ) {\displaystyle f(x)/\gcd(f(x),f'(x))} is a squarefree polynomial with the same factors as f ( x ) f(x),


#### Manuel Eberl (Oct 05 2023 at 13:30):

It's a bit more difficult than that in finite characteristic, I fear, since taking the derivative might kill some or all of the coefficients in the polynomial. For example, in characteristic $p$ the derivative of $x^p$ is $0$ and therefore dividing out the GCD of the polynomial and its derivative would just give us $1$.

#### Manuel Eberl (Oct 05 2023 at 13:31):

The ERF algorithm linked above detects this problem and fixes it. At least if I understood things correctly – I only skimmed it briefly.

#### Manuel Eberl (Dec 05 2023 at 10:17):

Just for the sake of completeness, this is now in the AFP:
https://www.isa-afp.org/entries/Perfect_Fields.html
https://www.isa-afp.org/entries/Elimination_Of_Repeated_Factors.html

Last updated: Dec 07 2023 at 16:21 UTC