mathlib documentation

field_theory.finite.polynomial

Polynomials over finite fields

source
theorem mv_polynomial.C_dvd_iff_zmod {σ : Type u_1} (n : ℕ) (φ : mv_polynomial σ ℤ) :
⇑mv_polynomial.C ↑n ∣ φ ↔ ⇑(mv_polynomial.map (int.cast_ring_hom (zmod n))) φ = 0

A polynomial over the integers is divisible by n : ℕ if and only if it is zero over zmod n.

source
theorem mv_polynomial.frobenius_zmod {σ : Type u_1} {p : ℕ} [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
⇑(frobenius (mv_polynomial σ (zmod p)) p) f = ⇑(mv_polynomial.expand p) f

source
theorem mv_polynomial.expand_zmod {σ : Type u_1} {p : ℕ} [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
⇑(mv_polynomial.expand p) f = f ^ p

source
def mv_polynomial.indicator {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (a : σ → K) :
mv_polynomial σ K

Equations
source
theorem mv_polynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (a : σ → K) :
⇑(mv_polynomial.eval a) (mv_polynomial.indicator a) = 1

source
theorem mv_polynomial.eval_indicator_apply_eq_zero {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (a b : σ → K) (h : a ≠ b) :
⇑(mv_polynomial.eval a) (mv_polynomial.indicator b) = 0

source
theorem mv_polynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (c : σ → K) :
(mv_polynomial.indicator c).degrees ≤ ∑ (s : σ), (fintype.card K - 1) •ℕ {s}

source
theorem mv_polynomial.indicator_mem_restrict_degree {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (c : σ → K) :
mv_polynomial.indicator c ∈ mv_polynomial.restrict_degree σ K (fintype.card K - 1)

source
def mv_polynomial.evalₗ (K : Type u_1) (σ : Type u_2) [field K] [fintype K] [fintype σ] :
mv_polynomial σ K →ₗ[K] (σ → K) → K

Equations
source
theorem mv_polynomial.evalₗ_apply {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (p : mv_polynomial σ K) (e : σ → K) :
⇑(mv_polynomial.evalₗ K σ) p e = ⇑(mv_polynomial.eval e) p

source
theorem mv_polynomial.map_restrict_dom_evalₗ {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] :
submodule.map (mv_polynomial.evalₗ K σ) (mv_polynomial.restrict_degree σ K (fintype.card K - 1)) = ⊤

source
@[instance]
def mv_polynomial.R.add_comm_group (σ K : Type u) [fintype σ] [field K] [fintype K] :
add_comm_group (mv_polynomial.R σ K)

source
@[instance]
def mv_polynomial.R.inhabited (σ K : Type u) [fintype σ] [field K] [fintype K] :
inhabited (mv_polynomial.R σ K)

source
def mv_polynomial.R (σ K : Type u) [fintype σ] [field K] [fintype K] :
Type u

Equations
source
@[instance]
def mv_polynomial.R.inst (σ K : Type u) [fintype σ] [field K] [fintype K] :
vector_space K (mv_polynomial.R σ K)

source
@[instance]
def mv_polynomial.decidable_restrict_degree (σ : Type u) [fintype σ] (m : ℕ) :
decidable_pred (λ (n : σ →₀ ℕ), n ∈ {n : σ →₀ ℕ | ∀ (i : σ), ⇑n i ≤ m})

Equations
source
theorem mv_polynomial.dim_R (σ K : Type u) [fintype σ] [field K] [fintype K] :
vector_space.dim K (mv_polynomial.R σ K) = ↑(fintype.card (σ → K))

source
def mv_polynomial.evalᵢ (σ K : Type u) [fintype σ] [field K] [fintype K] :
mv_polynomial.R σ K →ₗ[K] (σ → K) → K

Equations
source
theorem mv_polynomial.range_evalᵢ (σ K : Type u) [fintype σ] [field K] [fintype K] :
(mv_polynomial.evalᵢ σ K).range = ⊤

source
theorem mv_polynomial.ker_evalₗ (σ K : Type u) [fintype σ] [field K] [fintype K] :
(mv_polynomial.evalᵢ σ K).ker = ⊥

source
theorem mv_polynomial.eq_zero_of_eval_eq_zero (σ K : Type u) [fintype σ] [field K] [fintype K] (p : mv_polynomial σ K) (h : ∀ (v : σ → K), ⇑(mv_polynomial.eval v) p = 0) (hp : p ∈ mv_polynomial.restrict_degree σ K (fintype.card K - 1)) :
p = 0