# Documentation

Mathlib.FieldTheory.Finite.Polynomial

## Polynomials over finite fields #

theorem MvPolynomial.C_dvd_iff_zmod {σ : Type u_1} (n : ) (φ : ) :
MvPolynomial.C n φ ↑() φ = 0

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

theorem MvPolynomial.frobenius_zmod {σ : Type u_1} {p : } [Fact ()] (f : MvPolynomial σ (ZMod p)) :
↑(frobenius (MvPolynomial σ (ZMod p)) p) f = ↑() f
theorem MvPolynomial.expand_zmod {σ : Type u_1} {p : } [Fact ()] (f : MvPolynomial σ (ZMod p)) :
↑() f = f ^ p
def MvPolynomial.indicator {K : Type u_1} {σ : Type u_2} [] [] [] (a : σK) :

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

Instances For
theorem MvPolynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [] [] [] (a : σK) :
↑() () = 1
theorem MvPolynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [] [] [] (c : σK) :
Finset.sum Finset.univ fun s => () {s}
theorem MvPolynomial.indicator_mem_restrictDegree {K : Type u_1} {σ : Type u_2} [] [] [] (c : σK) :
theorem MvPolynomial.eval_indicator_apply_eq_zero {K : Type u_1} {σ : Type u_2} [] [] [] (a : σK) (b : σK) (h : a b) :
↑() () = 0
@[simp]
theorem MvPolynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) [] (p : ) (e : σK) :
↑() p e = ↑() p
def MvPolynomial.evalₗ (K : Type u_1) (σ : Type u_2) [] :
→ₗ[K] (σK) → K

MvPolynomial.eval as a K-linear map.

Instances For
theorem MvPolynomial.map_restrict_dom_evalₗ (K : Type u_1) (σ : Type u_2) [] [] [] :
def MvPolynomial.R (σ : Type u) (K : Type u) [] [] :

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

Instances For
noncomputable instance MvPolynomial.instAddCommGroupR (σ : Type u) (K : Type u) [] [] :
noncomputable instance MvPolynomial.instInhabitedR (σ : Type u) (K : Type u) [] [] :
def MvPolynomial.evalᵢ (σ : Type u) (K : Type u) [] [] :
→ₗ[K] (σK) → K

Evaluation in the mv_polynomial.R subtype.

Instances For
noncomputable instance MvPolynomial.decidableRestrictDegree (σ : Type u) (m : ) :
DecidablePred fun x => x {n | ∀ (i : σ), n i m}
theorem MvPolynomial.rank_R (σ : Type u) (K : Type u) [] [] [] :
Module.rank K () = ↑(Fintype.card (σK))
theorem MvPolynomial.finrank_R (σ : Type u) (K : Type u) [] [] [] :
= Fintype.card (σK)
theorem MvPolynomial.range_evalᵢ (σ : Type u) (K : Type u) [] [] [] :
theorem MvPolynomial.ker_evalₗ (σ : Type u) (K : Type u) [] [] [] :
theorem MvPolynomial.eq_zero_of_eval_eq_zero (σ : Type u) (K : Type u) [] [] [] (p : ) (h : ∀ (v : σK), ↑() p = 0) (hp : p ) :
p = 0