Polynomials over finite fields

theorem MvPolynomial.C_dvd_iff_zmod {σ : Type u_1} (n : ℕ) (φ : MvPolynomial σ ℤ) : ↑MvPolynomial.C ↑n ∣ φ ↔ ↑(MvPolynomial.map (Int.castRingHom (ZMod 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 (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)) : ↑(frobenius (MvPolynomial σ (ZMod p)) p) f = ↑(MvPolynomial.expand p) f

theorem MvPolynomial.expand_zmod {σ : Type u_1} {p : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)) : ↑(MvPolynomial.expand p) f = f ^ p

def MvPolynomial.indicator {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (a : σ → K) : MvPolynomial σ K

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

theorem MvPolynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (a : σ → K) : ↑(MvPolynomial.eval a) (MvPolynomial.indicator a) = 1

theorem MvPolynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (c : σ → K) : MvPolynomial.degrees (MvPolynomial.indicator c) ≤ Finset.sum Finset.univ fun s => (Fintype.card K - 1) • {s}

theorem MvPolynomial.indicator_mem_restrictDegree {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (c : σ → K) : MvPolynomial.indicator c ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1)

theorem MvPolynomial.eval_indicator_apply_eq_zero {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [Field K] (a : σ → K) (b : σ → K) (h : a ≠ b) : ↑(MvPolynomial.eval a) (MvPolynomial.indicator b) = 0

@[simp]

theorem MvPolynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) [CommSemiring K] (p : MvPolynomial σ K) (e : σ → K) : ↑(MvPolynomial.evalₗ K σ) p e = ↑(MvPolynomial.eval e) p

def MvPolynomial.evalₗ (K : Type u_1) (σ : Type u_2) [CommSemiring K] : MvPolynomial σ K →ₗ[K] (σ → K) → K

MvPolynomial.eval as a K-linear map.

theorem MvPolynomial.map_restrict_dom_evalₗ (K : Type u_1) (σ : Type u_2) [Field K] [Fintype K] [Finite σ] : Submodule.map (MvPolynomial.evalₗ K σ) (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)) = ⊤

def MvPolynomial.R (σ : Type u) (K : Type u) [Fintype K] [CommRing K] : Type u

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

noncomputable instance MvPolynomial.instAddCommGroupR (σ : Type u) (K : Type u) [Fintype K] [CommRing K] : AddCommGroup (MvPolynomial.R σ K)

noncomputable instance MvPolynomial.instModuleRToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupR (σ : Type u) (K : Type u) [Fintype K] [CommRing K] : Module K (MvPolynomial.R σ K)

noncomputable instance MvPolynomial.instInhabitedR (σ : Type u) (K : Type u) [Fintype K] [CommRing K] : Inhabited (MvPolynomial.R σ K)

def MvPolynomial.evalᵢ (σ : Type u) (K : Type u) [Fintype K] [CommRing K] : MvPolynomial.R σ K →ₗ[K] (σ → K) → K

Evaluation in the mv_polynomial.R subtype.

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) [Fintype K] [Field K] [Fintype σ] : Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))

instance MvPolynomial.instFiniteDimensionalRToCommRingToEuclideanDomainToDivisionRingInstAddCommGroupRInstModuleRToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupR (σ : Type u) (K : Type u) [Fintype K] [Field K] [Finite σ] : FiniteDimensional K (MvPolynomial.R σ K)

theorem MvPolynomial.finrank_R (σ : Type u) (K : Type u) [Fintype K] [Field K] [Fintype σ] : FiniteDimensional.finrank K (MvPolynomial.R σ K) = Fintype.card (σ → K)

theorem MvPolynomial.range_evalᵢ (σ : Type u) (K : Type u) [Fintype K] [Field K] [Finite σ] : LinearMap.range (MvPolynomial.evalᵢ σ K) = ⊤

theorem MvPolynomial.ker_evalₗ (σ : Type u) (K : Type u) [Fintype K] [Field K] [Finite σ] : LinearMap.ker (MvPolynomial.evalᵢ σ K) = ⊥

theorem MvPolynomial.eq_zero_of_eval_eq_zero (σ : Type u) (K : Type u) [Fintype K] [Field K] [Finite σ] (p : MvPolynomial σ K) (h : ∀ (v : σ → K), ↑(MvPolynomial.eval v) p = 0) (hp : p ∈ MvPolynomial.restrictDegree σ K (Fintype.card K - 1)) : p = 0