Primitive polynomials over finite fields

DefinitionPrimitive polynomial over a finite field#✓fully proved

Let \(F\) be a finite field with \(q\) elements, let \(f \in F[X]\), and let \(n\) be the degree of \(f\) (with \(n = 0\) if \(f = 0\)). Then \(f\) is primitive if it is monic, it is irreducible, and the class of \(X\) in the quotient ring \(F[X]/(f)\) has multiplicative order \(q^n - 1\).

def IsPrimitivePolynomial [Finite F] (f : F[X]) : Prop :=
  f.Monic ∧ Irreducible f ∧
    orderOf (AdjoinRoot.root f) = Nat.card F ^ f.natDegree - 1

Used by 6

Used byDefining characterization of primitive polynomials · Primitive polynomials via primitive roots of unity · Primitive polynomials are irreducible · Primitive polynomials are monic · Order of the root of a primitive polynomial · Primitive polynomials over \(\mathbb{Z}/p\mathbb{Z}\)

TheoremPrimitive polynomials are monic#✓fully proved

Every primitive polynomial over a finite field is monic.

theorem IsPrimitivePolynomial.monic {f : F[X]}
    (hf : f.IsPrimitivePolynomial) : f.Monic

Uses 1

Statement usesPrimitive polynomial over a finite field

TheoremPrimitive polynomials are irreducible#✓fully proved

Every primitive polynomial over a finite field is irreducible.

theorem IsPrimitivePolynomial.irreducible {f : F[X]}
    (hf : f.IsPrimitivePolynomial) : Irreducible f

Uses 1

Statement usesPrimitive polynomial over a finite field

TheoremOrder of the root of a primitive polynomial#✓fully proved

Let \(F\) be a finite field with \(q\) elements and let \(f \in F[X]\) be a primitive polynomial of degree \(n\). Then the class of \(X\) in the quotient ring \(F[X]/(f)\) has multiplicative order \(q^n - 1\).

theorem IsPrimitivePolynomial.root_orderOf {f : F[X]}
    (hf : f.IsPrimitivePolynomial) :
    orderOf (AdjoinRoot.root f) = Nat.card F ^ f.natDegree - 1

Uses 1

Statement usesPrimitive polynomial over a finite field

TheoremDefining characterization of primitive polynomials#✓fully proved

Let \(F\) be a finite field with \(q\) elements, let \(f \in F[X]\), and let \(n\) be the degree of \(f\) (with \(n = 0\) if \(f = 0\)). Then \(f\) is primitive if and only if \(f\) is monic, \(f\) is irreducible, and the class of \(X\) in the quotient ring \(F[X]/(f)\) has multiplicative order \(q^n - 1\).

theorem IsPrimitivePolynomial.iff {f : F[X]} :
    f.IsPrimitivePolynomial ↔ f.Monic ∧ Irreducible f ∧
      orderOf (AdjoinRoot.root f) = Nat.card F ^ f.natDegree - 1

Uses 1

Statement usesPrimitive polynomial over a finite field

TheoremPrimitive polynomials via primitive roots of unity#✓fully proved

Let \(F\) be a finite field with \(q\) elements, let \(f \in F[X]\), and let \(n\) be the degree of \(f\) (with \(n = 0\) if \(f = 0\)). Let \(\alpha\) be the class of \(X\) in the quotient ring \(F[X]/(f)\). Then \(f\) is primitive if and only if \(f\) is monic, \(f\) is irreducible, and \(\alpha\) is a primitive \((q^n - 1)\)-th root of unity, that is, \(\alpha^{q^n - 1} = 1\) and \(q^n - 1\) divides every natural number \(l\) with \(\alpha^l = 1\).

theorem IsPrimitivePolynomial.iff_isPrimitiveRoot {f : F[X]} :
    f.IsPrimitivePolynomial ↔ f.Monic ∧ Irreducible f ∧
      IsPrimitiveRoot (AdjoinRoot.root f)
        (Nat.card F ^ f.natDegree - 1)

Uses 1

Statement usesPrimitive polynomial over a finite field

TheoremPrimitive polynomials over \(\mathbb{Z}/p\mathbb{Z}\)#✓fully proved

Let \(p\) be a prime, let \(f\) be a polynomial over \(\mathbb{Z}/p\mathbb{Z}\), and let \(n\) be the degree of \(f\) (with \(n = 0\) if \(f = 0\)). Then \(f\) is primitive if and only if \(f\) is monic, \(f\) is irreducible, and the class of \(X\) in the quotient ring \((\mathbb{Z}/p\mathbb{Z})[X]/(f)\) has multiplicative order \(p^n - 1\).

theorem IsPrimitivePolynomial.zmod_iff (f : (ZMod p)[X]) :
    f.IsPrimitivePolynomial ↔ f.Monic ∧ Irreducible f ∧
      orderOf (AdjoinRoot.root f) = p ^ f.natDegree - 1

Sources

ATLAS Definition 3.14.

Uses 1

Statement usesPrimitive polynomial over a finite field

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.