Finite fields

Finite fields and polynomials over them: irreducible and primitive polynomials, permutation polynomials, and the arithmetic of squares.

• Permutation polynomials
• Primitive polynomials over finite fields
• Searching for irreducible polynomials over GF(2)

TheoremA square avoiding \(0\), \(1\) and \(-1\) in a finite field#✓fully proved

If \(F\) is a finite field with more than five elements, then there is an element \(r \in F\) with \(r^2 \neq 0\), \(r^2 \neq 1\) and \(r^2 \neq -1\).

theorem exists_sq_ne_zero_one_neg_one {F : Type*} [Field F] [Fintype F]
    (hF : 5 < Fintype.card F) :
    ∃ r : F, r ^ 2 ≠ 0 ∧ r ^ 2 ≠ 1 ∧ r ^ 2 ≠ -1

TheoremPolynomial evaluation commutes with the Frobenius power#✓fully proved

Evaluating p at x ^ q equals the q-th power of evaluating p at x, where q is the cardinality of the finite field F.

theorem Polynomial.aeval_pow_card_eq_pow_card (F : Type*) [Field F] [Fintype F]
    (E : Type*) [CommRing E] [Algebra F E] (p : Polynomial F) (x : E) :
    Polynomial.aeval (x ^ Fintype.card F) p = (Polynomial.aeval x p) ^ Fintype.card F

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.