Integer polynomials modulo X^p - 1

Main definitions

• CyclicIntRing: the integer polynomial quotient.
• CyclicIntRing.coeff: coefficients in the unique representative of degree less than p.

Main results

• CyclicIntRing.coeff_x_pow: powers have a single coefficient at the residue of their exponent.

References

Adapted from Anthropic's Hashing.lean.

@[reducible, inline]

abbrev Cslib.CyclicIntRing (p : ℕ) : Type

The quotient ring ℤ[X]/(X^p - 1).

noncomputable def Cslib.CyclicIntRing.x (p : ℕ) : CyclicIntRing p

The element x of ℤ[x]/(x^p − 1).

noncomputable def Cslib.CyclicIntRing.coeff {p : ℕ} (hp : p ≠ 0) (r : ℕ) : CyclicIntRing p →ₗ[ℤ] ℤ

The coefficient of degree r in an element z of the quotient, as a linear map. It is the coefficient of x^r in the unique polynomial of degree less than p that represents z (Mathlib's AdjoinRoot.modByMonicHom gives that polynomial; it asks for the fact that x^p − 1 is monic, which holds as p ≠ 0).

theorem Cslib.CyclicIntRing.coeff_apply {p : ℕ} (hp : p ≠ 0) (r : ℕ) (z : CyclicIntRing p) : (coeff hp r) z = ((AdjoinRoot.modByMonicHom ⋯) z).coeff r

The coefficient, in terms of the representing polynomial.

theorem Cslib.CyclicIntRing.coeff_x_pow {p : ℕ} (hp : p ≠ 0) (k r : ℕ) : (coeff hp r) (x p ^ k) = if r = k % p then 1 else 0

The coefficient of x^r in the power x^k of ℤ[x]/(x^p − 1) is 1 if r = k mod p and 0 otherwise.