mathlib documentation

field_theory.finite.polynomial

Polynomials over finite fields #

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

theorem mv_polynomial.frobenius_zmod {σ : Type u_1} {p : } [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
theorem mv_polynomial.expand_zmod {σ : Type u_1} {p : } [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
def mv_polynomial.indicator {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (a : σ → K) :
Equations
theorem mv_polynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (a : σ → K) :
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) :
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}
theorem mv_polynomial.indicator_mem_restrict_degree {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (c : σ → K) :
def mv_polynomial.evalₗ (K : Type u_1) (σ : Type u_2) [field K] [fintype K] [fintype σ] :
mv_polynomial σ K →ₗ[K] (σ → K) → K
Equations
theorem mv_polynomial.evalₗ_apply {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [fintype σ] (p : mv_polynomial σ K) (e : σ → K) :
@[instance]
@[instance]
def mv_polynomial.R.inhabited (σ K : Type u) [fintype σ] [field K] [fintype K] :
def mv_polynomial.R (σ K : Type u) [fintype σ] [field K] [fintype K] :
Type u
Equations
@[instance]
def mv_polynomial.R.module (σ K : Type u) [fintype σ] [field K] [fintype K] :
@[instance]
def mv_polynomial.decidable_restrict_degree (σ : Type u) [fintype σ] (m : ) :
decidable_pred (λ (n : σ →₀ ), n {n : σ →₀ | ∀ (i : σ), n i m})
Equations
theorem mv_polynomial.dim_R (σ K : Type u) [fintype σ] [field K] [fintype K] :
@[instance]
theorem mv_polynomial.finrank_R (σ K : Type u) [fintype σ] [field K] [fintype K] :
def mv_polynomial.evalᵢ (σ K : Type u) [fintype σ] [field K] [fintype K] :
mv_polynomial.R σ K →ₗ[K] (σ → K) → K
Equations
theorem mv_polynomial.range_evalᵢ (σ K : Type u) [fintype σ] [field K] [fintype K] :
theorem mv_polynomial.ker_evalₗ (σ K : Type u) [fintype σ] [field K] [fintype K] :
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