Abstract

This article formalises the Elimination of Repeated Factors (ERF) Algorithm. This is an algorithm to find the square-free part of polynomials over perfect fields. Notably, this encompasses all fields of characteristic 0 and all finite fields. For fields with characteristic 0, the ERF algorithm proceeds similarly to the classical Yun algorithm. However, for fields with non-zero characteristic p, Yun’s algorithm can fail because the derivative of a non-zero polynomial can be 0. The ERF algorithm detects this case and therefore also works in this more general setting. To state the ERF Algorithm in this general form, we build on the entry on perfect fields. We show that the ERF algorithm is correct and returns a list of pairwise coprime square-free polynomials whose product is the input polynomial. Indeed, through this, the ERF algorithm also yields executable code for calculating the square-free part of a polynomial (denoted by the function radical).

BibTeX

@article{Elimination_Of_Repeated_Factors-AFP,
  author  = {Katharina Kreuzer and Manuel Eberl},
  title   = {Elimination of Repeated Factors Algorithm},
  journal = {Archive of Formal Proofs},
  month   = {November},
  year    = {2023},
  note    = {\url{https://isa-afp.org/entries/Elimination_Of_Repeated_Factors.html},
             Formal proof development},
  ISSN    = {2150-914x},
}