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)) :
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) :
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) [comm_semiring K] (p : mv_polynomial σ K) (e : σ → K) :
noncomputable def mv_polynomial.evalₗ (K : Type u_1) (σ : Type u_2) [comm_semiring K] :
mv_polynomial σ K →ₗ[K] (σ → K) → K

mv_polynomial.eval as a K-linear map.

Equations
@[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] :
noncomputable def mv_polynomial.evalᵢ (σ K : Type u) [fintype K] [comm_ring K] :
mv_polynomial.R σ 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 σ] :
@[protected, instance]
theorem mv_polynomial.finrank_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
theorem mv_polynomial.eq_zero_of_eval_eq_zero (σ K : Type u) [fintype K] [field K] [finite σ] (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