Permutation polynomials
DefinitionPermutation polynomial over a finite field#✓fully proved
A polynomial \(f\) over a finite field \(F\) is a permutation polynomial when its evaluation map \(F \to F\), \(x \mapsto f(x)\), is bijective.
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
Used by 8
DefinitionPolynomial complete to level \(k\)#✓fully proved
Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. The polynomial \(f\) is complete to level \(k\) (\(k\)-complete) when \(f + iX\) is a permutation polynomial for every natural number \(i \le k\), where \(i\) is viewed as an element of \(F\).
The source considers only positive levels \(k\); here every natural level is allowed, and completeness to level \(0\) says that \(f\) itself is a permutation polynomial.
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:28
TheoremUnfolded form of \(k\)-completeness#✓fully proved
Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. Then \(f\) is complete to level \(k\) if and only if for every natural number \(i \le k\) the map \(F \to F\), \(x \mapsto (f + iX)(x)\), is bijective, where \(i\) is viewed as an element of \(F\).
theorem isKComplete_iff {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) :
IsKComplete f k ↔ ∀ i : ℕ, i ≤ k →
Function.Bijective fun x =>
(f + Polynomial.C (i : F) * Polynomial.X).eval x
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:38
Uses 1
TheoremCompleteness at a lower level#✓fully proved
Let \(F\) be a finite field, \(f \in F[X]\) and let \(j \le k\) be natural numbers. If \(f\) is complete to level \(k\), then \(f\) is complete to level \(j\).
theorem isKComplete_mono {F : Type*} [Field F] [Finite F] {f : Polynomial F}
{j k : ℕ} (h : IsKComplete f k) (hle : j ≤ k) : IsKComplete f j
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:38
Uses 1
TheoremCompleteness at level zero#✓fully proved
Let \(F\) be a finite field and \(f \in F[X]\). Then \(f\) is complete to level \(0\) if and only if \(f\) is a permutation polynomial.
theorem isKComplete_zero {F : Type*} [Field F] [Finite F] (f : Polynomial F) :
IsKComplete f 0 ↔ IsPermutationPolynomial f
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:38
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:28
Uses 2
TheoremCompleteness at the next level#✓fully proved
Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. Then \(f\) is complete to level \(k + 1\) if and only if \(f\) is complete to level \(k\) and \(f + (k + 1)X\) is a permutation polynomial, where \(k + 1\) is viewed as an element of \(F\).
theorem isKComplete_succ_iff {F : Type*} [Field F] [Finite F]
(f : Polynomial F) (k : ℕ) :
IsKComplete f (k + 1) ↔ IsKComplete f k ∧
IsPermutationPolynomial
(f + Polynomial.C ((k + 1 : ℕ) : F) * Polynomial.X)
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:38
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:28
Uses 2
TheoremA \(k\)-complete polynomial is a permutation polynomial#✓fully proved
Let \(F\) be a finite field, \(f \in F[X]\) and \(k\) a natural number. If \(f\) is complete to level \(k\), then \(f\) is a permutation polynomial.
theorem isKComplete_self {F : Type*} [Field F] [Finite F] {f : Polynomial F}
{k : ℕ} (h : IsKComplete f k) : IsPermutationPolynomial f
def IsKComplete {F : Type*} [Field F] [Finite F] (f : Polynomial F)
(k : ℕ) : Prop :=
∀ i : ℕ, i ≤ k → IsPermutationPolynomial (f + Polynomial.C (i : F) * Polynomial.X)
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:38
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:28
Uses 2
TheoremHermite–Dickson criterion#✓fully proved
Let \(\mathbb{F}_q\) be a finite field with \(q\) elements and characteristic \(p\), and let \(f \in \mathbb{F}_q[X]\). Then \(f\) is a permutation polynomial of \(\mathbb{F}_q\), that is, \(x \mapsto f(x)\) is a bijection of \(\mathbb{F}_q\), if and only if \(f\) has exactly one root in \(\mathbb{F}_q\) and, for every integer \(t\) with \(1 \le t \le q - 2\) and \(p \nmid t\), the remainder of \(f^t\) upon division by \(X^q - X\) has degree at most \(q - 2\).
theorem hermite_dickson_permutation_criterion
{p : ℕ} {Fq : Type*} [Field Fq] [Fintype Fq] [DecidableEq Fq] [CharP Fq p]
[Fact p.Prime] (hq : 2 ≤ Fintype.card Fq) (f : Polynomial Fq) :
let q := Fintype.card Fq
Polynomial.IsPermutationPolynomial f ↔
(Finset.univ.filter (fun x => Polynomial.eval x f = 0)).card = 1 ∧
∀ t : ℕ, 1 ≤ t → t ≤ q - 2 → ¬ p ∣ t →
Polynomial.natDegree ((f ^ t) % (Polynomial.X ^ q - Polynomial.X)) ≤ q - 2
def IsPermutationPolynomial {F : Type*} [Field F] [Finite F]
(f : Polynomial F) : Prop :=
Function.Bijective fun x => f.eval x
MathlibExt/FieldTheory/Finite/PermutationPolynomial.lean:28
Sources
- Brian G. Kronenthal, "An Integer Sequence Motivated by Generalized Quadrangles", Journal of Integer Sequences 18 (2015), Article 15.7.8, https://cs.uwaterloo.ca/journals/JIS/VOL18/Kronenthal/kron3.tex, Hermite–Dickson statement at lines 120–126.
Uses 1
TheoremMonomial permutation polynomials of a finite field#●ready to prove
Let \(K\) be a finite field with \(q\) elements and let \(d \ge 1\) be an integer. Then \(X^d\) is a permutation polynomial of \(K\) if and only if \(\gcd(d, q - 1) = 1\).
The hypothesis \(d \ge 1\) is needed: for \(d = 0\) and \(q = 2\) the condition \(\gcd(d, q - 1) = 1\) holds, but \(X^0 = 1\) is constant.
public theorem_wanted isPermutationPolynomial_X_pow_iff_coprime {K : Type*} [Field K]
[Fintype K] {d : ℕ} (hd : 0 < d) :
(X ^ d : K[X]).IsPermutationPolynomial ↔ d.Coprime (Fintype.card K - 1)
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 2.
Uses 1
TheoremPower-sum criterion for distinct elements of a finite field#●ready to prove
Let \(K\) be a finite field with \(q\) elements and let \(a_1, \dots, a_q \in K\). Then \(a_1, \dots, a_q\) are pairwise distinct if and only if \(\sum_{i=1}^{q} a_i^t = 0\) for every \(t = 0, 1, \dots, q - 2\) and \(\sum_{i=1}^{q} a_i^{q-1} = -1\), where \(0^0 = 1\).
public theorem_wanted injective_iff_sum_pow_eq {K : Type*} [Field K] [Fintype K]
(a : Fin (Fintype.card K) → K) :
Function.Injective a ↔
(∀ t : ℕ, t < Fintype.card K - 1 → ∑ i, a i ^ t = 0) ∧
∑ i, a i ^ (Fintype.card K - 1) = -1
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 3.
TheoremAlternating binomial sums of powers#●ready to prove
Let \(x, y, k \in \mathbb{C}\) and let \(n, m\) be positive integers. If \(n = m\), then
and if \(m < n\), then \(\sum_{i=0}^{n} (-1)^i \binom{n}{i} (kx + iy)^m = 0\).
public theorem_wanted sum_neg_one_pow_choose_mul_pow (x y k : ℂ) {n m : ℕ} (hn : 0 < n)
(hm : 0 < m) :
(n = m → ∑ i ∈ Finset.range (n + 1),
(-1 : ℂ) ^ i * (n.choose i : ℂ) * (k * x + i * y) ^ m =
(-1) ^ n * y ^ n * (n.factorial : ℂ)) ∧
(m < n → ∑ i ∈ Finset.range (n + 1),
(-1 : ℂ) ^ i * (n.choose i : ℂ) * (k * x + i * y) ^ m = 0)
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Theorem 3.
TheoremShifted power-sum permutation polynomials of a prime field#●ready to prove
Let \(p\) be an odd prime and let \(k, t, a\) be positive integers with \(\gcd(a + 1, p - 1) = 1\) and \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(p - 1 \nmid t\) or \(p^2 \mid k - 1\). Then the polynomial \(\sum_{n=1}^{k} n^t X^{n+a}\), with coefficients reduced modulo \(p\), is a permutation polynomial of \(\mathbb{F}_p\).
public theorem_wanted isPermutationPolynomial_sum_pow_mul_X_pow_add {p : ℕ} [Fact p.Prime]
(hp : p ≠ 2) {k t a : ℕ} (hk : 0 < k) (ht : 0 < t) (ha : 0 < a)
(hka : (a + 1).Coprime (p - 1)) (hkcong : k ≡ 1 [MOD p * (p - 1)])
(hcases : ¬(p - 1) ∣ t ∨ p ^ 2 ∣ k - 1) :
(∑ n ∈ Finset.Icc 1 k, C ((n : ZMod p) ^ t) * X ^ (n + a)).IsPermutationPolynomial
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 1.
Uses 1
TheoremDilated power-sum permutation polynomials of a prime field#●ready to prove
Let \(p\) be an odd prime and let \(k, t, a\) be positive integers with \(p \nmid a\), \(\gcd(a, p - 1) = 1\) and \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(p - 1 \nmid t\) or \(p^2 \mid k - 1\). Then the polynomial \(\sum_{n=1}^{k} (an)^t X^{an}\), with coefficients reduced modulo \(p\), is a permutation polynomial of \(\mathbb{F}_p\).
public theorem_wanted isPermutationPolynomial_sum_mul_pow_mul_X_pow_mul {p : ℕ}
[Fact p.Prime] (hp : p ≠ 2) {k t a : ℕ} (hk : 0 < k) (ht : 0 < t) (ha : 0 < a)
(hpa : ¬p ∣ a) (hap : a.Coprime (p - 1)) (hkcong : k ≡ 1 [MOD p * (p - 1)])
(hcases : ¬(p - 1) ∣ t ∨ p ^ 2 ∣ k - 1) :
(∑ n ∈ Finset.Icc 1 k,
C (((a * n : ℕ) : ZMod p) ^ t) * X ^ (a * n)).IsPermutationPolynomial
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 3.
Uses 1
TheoremRational form of the power-weighted geometric sum#●ready to prove
For positive integers \(t\) and \(k\), the following identity holds in \(\mathbb{Z}[X]\):
Equivalently, for every \(x \ne 1\) the value \(h_t^k(x) = \sum_{n=1}^{k} n^t x^n\) is the right-hand side at \(x\) divided by \((1 - x)^{t+1}\), which is the form the source states.
public theorem_wanted one_sub_X_pow_mul_sum_pow_mul_X_pow (t k : ℕ) (ht : 0 < t) (hk : 0 < k) :
(1 - X : ℤ[X]) ^ (t + 1) * ∑ n ∈ Finset.Icc 1 k, C ((n : ℤ) ^ t) * X ^ n =
∑ n ∈ Finset.Icc 1 t, C (∑ i ∈ Finset.range n,
(-1) ^ i * ((t + 1).choose i : ℤ) * ((n : ℤ) - i) ^ t) * X ^ n +
∑ m ∈ Finset.Icc 1 (t + 1), C (∑ i ∈ Finset.Icc m (t + 1),
(-1) ^ i * ((t + 1).choose i : ℤ) * ((k : ℤ) + m - i) ^ t) * X ^ (k + m)
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Lemma 4.
TheoremVishwakarma–Singh congruence for ordered partitions#●ready to prove
Let \(p\) be an odd prime and let \(k, s, t\) be positive integers with \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\), such that \(p^2 \mid k - 1\) whenever \(p - 1 \mid t\). Let \(\mu = \lfloor ks/(p - 1) \rfloor\). Then
where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{1, \dots, k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).
The source states the hypothesis \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\), the range of Hermite's criterion used in its proof; with that hypothesis the claim fails, e.g. for \(p = 3\), \(k = 1\), \(s = 2\), \(t = 1\) the sum is \(1\).
public theorem_wanted prime_dvd_sum_compositions_prod_pow {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
{k s t : ℕ} (hk : 0 < k) (hs : 0 < s) (hsp : s ≤ p - 2) (ht : 0 < t)
(hkcong : k ≡ 1 [MOD p * (p - 1)]) (hcases : (p - 1) ∣ t → p ^ 2 ∣ k - 1) :
p ∣ ∑ j ∈ Finset.Icc 1 (k * s / (p - 1)),
∑ ω ∈ (Fintype.piFinset fun _ : Fin s => Finset.Icc 1 k).filter
(fun ω => ∑ i, ω i = j * (p - 1)),
(∏ i, ω i) ^ t
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Theorem 1.
TheoremVishwakarma–Singh congruence for ordered partitions, linear case#●ready to prove
Let \(p\) be an odd prime and let \(k, s\) be positive integers with \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\). Let \(\mu = \lfloor ks/(p - 1) \rfloor\). Then
where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{1, \dots, k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).
This is the case \(t = 1\) of the source's Theorem 1. The source states the hypothesis \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\); with that hypothesis the claim fails, e.g. for \(p = 3\), \(k = 7\), \(s = 2\) the sum is \(400 \equiv 1 \pmod{3}\).
public theorem_wanted prime_dvd_sum_compositions_prod {p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2)
{k s : ℕ} (hk : 0 < k) (hs : 0 < s) (hsp : s ≤ p - 2) (hkcong : k ≡ 1 [MOD p * (p - 1)]) :
p ∣ ∑ j ∈ Finset.Icc 1 (k * s / (p - 1)),
∑ ω ∈ (Fintype.piFinset fun _ : Fin s => Finset.Icc 1 k).filter
(fun ω => ∑ i, ω i = j * (p - 1)),
∏ i, ω i
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 2.
TheoremVishwakarma–Singh congruence for ordered partitions into multiples#●ready to prove
Let \(p\) be an odd prime and let \(a, k, s, t\) be positive integers with \(\gcd(a, p - 1) = 1\), \(s \le p - 2\) and \(k \equiv 1 \pmod{p(p-1)}\), such that \(p^2 \mid k - 1\) whenever \(p - 1 \mid t\). Let \(\mu = \lfloor aks/(p - 1) \rfloor\). Then
where for each \(j\) the inner sum runs over all \(s\)-tuples \(\omega = (\omega_1, \dots, \omega_s)\) with entries in \(\{an : 1 \le n \le k\}\) and \(\omega_1 + \cdots + \omega_s = j(p - 1)\).
The source states this with two differences. It assumes \(s \not\equiv 0 \pmod{p}\) in place of \(s \le p - 2\); with that hypothesis the claim fails, e.g. for \(a = 1\), \(p = 3\), \(k = 7\), \(s = 2\), \(t = 1\). It takes \(\mu = \lfloor ks/(p - 1) \rfloor\); with that bound the claim fails for \(a > 1\), e.g. for \(p = 5\), \(a = 3\), \(k = 21\), \(s = t = 1\) the sum is \(12\). The bound \(\lfloor aks/(p - 1) \rfloor\) covers every multiple of \(p - 1\) up to \(aks\), the degree of the \(s\)-th power of \(\sum_{n=1}^{k} (an)^t X^{an}\), to which the proof applies Hermite's criterion.
public theorem_wanted prime_dvd_sum_compositions_mul_prod_pow {p : ℕ} (hp : p.Prime)
(hp2 : p ≠ 2) {a k s t : ℕ} (ha : 0 < a) (hap : a.Coprime (p - 1)) (hk : 0 < k) (hs : 0 < s)
(hsp : s ≤ p - 2) (ht : 0 < t) (hkcong : k ≡ 1 [MOD p * (p - 1)])
(hcases : (p - 1) ∣ t → p ^ 2 ∣ k - 1) :
p ∣ ∑ j ∈ Finset.Icc 1 (a * k * s / (p - 1)),
∑ ω ∈ (Fintype.piFinset fun _ : Fin s => (Finset.Icc 1 k).image (a * ·)).filter
(fun ω => ∑ i, ω i = j * (p - 1)),
(∏ i, ω i) ^ t
Sources
- Chandan Kumar Vishwakarma and Rajesh P. Singh, A Congruence Identity on Ordered Partitions Using Permutation Polynomials, INTEGERS 24 (2024), Article A12, Corollary 4.
TheoremPower sums over \(\mathbb{Z}/p\mathbb{Z}\)#●ready to prove
Let \(p\) be a prime and \(t\) a positive integer. Then \(\sum_{a \in \mathbb{Z}/p\mathbb{Z}} a^t\) equals \(-1\) if \(p - 1\) divides \(t\), and \(0\) otherwise.
theorem_wanted sum_zmod_pow_eq_ite
(p t : ℕ) [NeZero p] (hp : p.Prime) (ht : 0 < t) :
(∑ a : ZMod p, a ^ t) = if (p - 1) ∣ t then -1 else 0
Sources
- Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form
∑_{n=1}^k h(n) X^n", Lemma 1.
TheoremPermutation polynomials \(\sum_{n=1}^k n^t X^n\) over \(\mathbb{F}_p\)#●ready to prove
Let \(p\) be an odd prime and let \(k\) and \(t\) be positive integers with \(k \equiv 1 \pmod{p(p-1)}\). Suppose that \(k \equiv 1 \pmod{p^2}\) or that \(p - 1\) does not divide \(t\). Then the map \(c \mapsto \sum_{n=1}^{k} n^t c^n\) is a bijection from \(\mathbb{Z}/p\mathbb{Z}\) to itself.
Ding and Zieve quote this result from an earlier paper.
theorem_wanted bijective_sum_pow_mul_pow_zmod
(p k t : ℕ) (hp : p.Prime) (hpodd : p % 2 = 1)
(hk : 0 < k) (ht : 0 < t)
(hkcong : k % (p * (p - 1)) = 1)
(hcases : k % (p ^ 2) = 1 ∨ ¬(p - 1) ∣ t) :
Function.Bijective
(fun c : ZMod p =>
∑ n ∈ Finset.Icc 1 k, (n : ZMod p) ^ t * c ^ n)
Sources
- Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form
∑_{n=1}^k h(n) X^n", Theorem 1.
TheoremWhen \(\sum_{n=1}^k h(n) X^n\) induces the identity on \(\mathbb{F}_q\)#●ready to prove
Let \(p\) be a prime, \(\ell \ge 1\) and \(q = p^\ell > 2\), and let \(K\) be a finite field of characteristic \(p\) with \(q\) elements. Let \(k\) be a positive integer with \(k \equiv 1 \pmod{p(q-1)}\) and let \(h \in K[X]\), with degree \(d\) (taken to be \(0\) when \(h = 0\)) and coefficient \(h_i\) of \(X^i\). Then \(\sum_{n=1}^{k} h(n)\,c^n = c\) for every \(c \in K\) if and only if \(h(1) = 1\) and either \(k \equiv 1 \pmod{p^2}\) or \(\sum_{j=1}^{\lfloor d/(p-1) \rfloor} h_{j(p-1)} = 0\).
theorem_wanted finiteField_sum_eval_mul_pow_eq_id_iff
(K : Type*) [Field K] [Fintype K] (p ℓ : ℕ) [CharP K p]
(hp : p.Prime) (hℓ : 0 < ℓ)
(hcard : Fintype.card K = p ^ ℓ) (hq : 2 < p ^ ℓ)
(k : ℕ) (hk : 0 < k)
(hkcong : k % (p * (p ^ ℓ - 1)) = 1)
(h : Polynomial K) :
(∀ c : K, (∑ n ∈ Finset.Icc 1 k, h.eval (n : K) * c ^ n) = c) ↔
h.eval 1 = 1 ∧
(k % (p ^ 2) = 1 ∨
(∑ j ∈ Finset.Icc 1 (h.natDegree / (p - 1)),
h.coeff (j * (p - 1))) = 0)
Sources
- Zhiguo Ding and Michael E. Zieve, "Permutation Polynomials of the Form
∑_{n=1}^k h(n) X^n", Theorem 2.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.