# Documentation

## 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.

Equations
• = Finset.prod Finset.univ fun (n : σ) => 1 - ( - MvPolynomial.C (a n)) ^ ()
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.

Equations
• = { toAddHom := { toFun := fun (p : ) (e : σK) => p, map_add' := }, map_smul' := }
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.

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

Evaluation in the mv_polynomial.R subtype.

Equations
Instances For
noncomputable instance MvPolynomial.decidableRestrictDegree (σ : Type u) (m : ) :
DecidablePred fun (x : σ →₀ ) => x {n : σ →₀ | ∀ (i : σ), n i m}
Equations
• = id inferInstance
theorem MvPolynomial.rank_R (σ : Type u) (K : Type u) [] [] [] :
Module.rank K () = (Fintype.card (σK))
Equations
• =
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