# mathlibdocumentation

field_theory.finite.polynomial

## Polynomials over finite fields #

theorem mv_polynomial.C_dvd_iff_zmod {σ : Type u_1} (n : ) (φ : ) :
φ = 0

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 : (zmod p)) :
(frobenius (zmod p)) p) f =
theorem mv_polynomial.expand_zmod {σ : Type u_1} {p : } [fact (nat.prime p)] (f : (zmod p)) :
= f ^ p
noncomputable def mv_polynomial.indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (a : σ → K) :

Over a field, this is the indicator function as an mv_polynomial.

Equations
theorem mv_polynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (a : σ → K) :
theorem mv_polynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (c : σ → K) :
finset.univ.sum (λ (s : σ), - 1) {s})
theorem mv_polynomial.indicator_mem_restrict_degree {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (c : σ → K) :
theorem mv_polynomial.eval_indicator_apply_eq_zero {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [field K] (a b : σ → K) (h : a b) :
@[simp]
theorem mv_polynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) (p : K) (e : σ → K) :
σ) p e = p
noncomputable def mv_polynomial.evalₗ (K : Type u_1) (σ : Type u_2)  :
→ₗ[K] (σ → K) → K

mv_polynomial.eval as a K-linear map.

Equations
theorem mv_polynomial.map_restrict_dom_evalₗ {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [finite σ] :
- 1)) =
@[protected, instance]
noncomputable def mv_polynomial.R.add_comm_group (σ K : Type u) [fintype K] [comm_ring K] :
@[protected, instance]
noncomputable def mv_polynomial.R.inhabited (σ K : Type u) [fintype K] [comm_ring K] :
def mv_polynomial.R (σ K : Type u) [fintype K] [comm_ring K] :
Type u

The submodule of multivariate polynomials whose degree of each variable is strictly less than the cardinality of K.

Equations
Instances for mv_polynomial.R
@[protected, instance]
noncomputable def mv_polynomial.R.module (σ K : Type u) [fintype K] [comm_ring K] :
K)
noncomputable def mv_polynomial.evalᵢ (σ K : Type u) [fintype K] [comm_ring K] :
→ₗ[K] (σ → K) → K

Evaluation in the mv_polynomial.R subtype.

Equations
@[protected, instance]
noncomputable def mv_polynomial.decidable_restrict_degree (σ : Type u) (m : ) :
decidable_pred (λ (_x : σ →₀ ), _x {n : σ →₀ | ∀ (i : σ), n i m})
Equations
theorem mv_polynomial.dim_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
K) = (fintype.card (σ → K))
@[protected, instance]
def mv_polynomial.R.finite_dimensional (σ K : Type u) [fintype K] [field K] [finite σ] :
theorem mv_polynomial.finrank_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
= fintype.card (σ → K)
theorem mv_polynomial.range_evalᵢ (σ K : Type u) [fintype K] [field K] [finite σ] :
theorem mv_polynomial.ker_evalₗ (σ K : Type u) [fintype K] [field K] [finite σ] :
theorem mv_polynomial.eq_zero_of_eval_eq_zero (σ K : Type u) [fintype K] [field K] [finite σ] (p : K) (h : ∀ (v : σ → K), p = 0) (hp : p - 1)) :
p = 0