def Hex.DensePoly.cyclicModulus {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) : DensePoly R

The monic polynomial x^n - 1 used for cyclic convolution.

Equations

• Hex.DensePoly.cyclicModulus n = Hex.DensePoly.monomial n 1 - 1

def Hex.DensePoly.negacyclicModulus {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) : DensePoly R

The monic polynomial x^n + 1 used for negacyclic convolution.

Equations

• Hex.DensePoly.negacyclicModulus n = Hex.DensePoly.monomial n 1 + 1

theorem Hex.DensePoly.size_cyclicModulus {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) : (cyclicModulus n).size = n + 1

Over a nontrivial ring, the positive-length cyclic modulus has size n + 1.

theorem Hex.DensePoly.size_negacyclicModulus {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) : (negacyclicModulus n).size = n + 1

Over a nontrivial ring, the positive-length negacyclic modulus has size n + 1.

theorem Hex.DensePoly.cyclicModulus_monic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) : (cyclicModulus n).Monic

The positive-length cyclic modulus is monic over a nontrivial ring.

theorem Hex.DensePoly.negacyclicModulus_monic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) : (negacyclicModulus n).Monic

The positive-length negacyclic modulus is monic over a nontrivial ring.

theorem Hex.DensePoly.cyclicModulus_dvd_monomial_sub {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n i : Nat) (hn : 0 < n) (c : R) : cyclicModulus n ∣ monomial i c - monomial (i % n) c

A monomial and the monomial obtained by reducing its exponent modulo n are congruent modulo x^n - 1.

theorem Hex.DensePoly.foldl_monomials_eq {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (p : DensePoly R) : List.foldl (fun (q : DensePoly R) (i : Nat) => q + monomial i (p.coeff i)) 0 (List.range p.size) = p

Summing a polynomial's coefficient monomials reconstructs the polynomial.

theorem Hex.DensePoly.cyclicModulus_dvd_sub_fold {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (p : DensePoly R) : cyclicModulus n ∣ p - ofCoeffs (cyclicCoeffs n p)

Cyclic folding preserves the residue modulo x^n - 1.

theorem Hex.DensePoly.ofCoeffs_cyclicCoeffs_eq_modByMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) (p : DensePoly R) : ofCoeffs (cyclicCoeffs n p) = p.modByMonic (cyclicModulus n) ⋯

The cyclic coefficient fold is exactly the canonical monic remainder modulo x^n - 1.

theorem Hex.DensePoly.mulCyclic_eq_modByMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) (a b : DensePoly R) : mulCyclic plan n hn a b = (a * b).modByMonic (cyclicModulus n) ⋯

Planned cyclic multiplication is polynomial remainder modulo x^n - 1.

theorem Hex.DensePoly.negacyclicModulus_dvd_monomial_sub {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n i : Nat) (hn : 0 < n) (c : R) : negacyclicModulus n ∣ monomial i c - negacyclicResidue n i c

A monomial and its signed exponent reduction are congruent modulo x^n + 1.

theorem Hex.DensePoly.negacyclicModulus_dvd_sub_fold {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (p : DensePoly R) : negacyclicModulus n ∣ p - ofCoeffs (negacyclicCoeffs n p)

Negacyclic folding preserves the residue modulo x^n + 1.

theorem Hex.DensePoly.ofCoeffs_negacyclicCoeffs_eq_modByMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) (p : DensePoly R) : ofCoeffs (negacyclicCoeffs n p) = p.modByMonic (negacyclicModulus n) ⋯

The negacyclic coefficient fold is exactly the canonical monic remainder modulo x^n + 1.

theorem Hex.DensePoly.mulNegacyclic_eq_modByMonic {R : Type u} [DecidableEq R] [Lean.Grind.CommRing R] (plan : MulPlan R) (n : Nat) (hn : 0 < n) (hone : 1 ≠ 0) (a b : DensePoly R) : mulNegacyclic plan n hn a b = (a * b).modByMonic (negacyclicModulus n) ⋯

Planned negacyclic multiplication is polynomial remainder modulo x^n + 1.