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 :)

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.

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

(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)

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

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

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

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

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" )

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

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

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

Hi thanks for the answer!

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 :) ).

Tobias Rothmann said:

Hi thanks for the answer!

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. :)

Emin Karayel said:

Tobias Rothmann said:

Hi thanks for the answer!

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 :)

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),
```

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$.

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

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