Polynomials over finite fields

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

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

noncomputable 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) : (eval a) (indicator a) = 1

theorem MvPolynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (c : σ → K) : (indicator c).degrees ≤ ∑ 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) : indicator c ∈ 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 b : σ → K) (h : a ≠ b) : (eval a) (indicator b) = 0

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

MvPolynomial.eval as a K-linear map.

@[simp]

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

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

def MvPolynomial.R (σ 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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

Evaluation in the MvPolynomial.R subtype.

@[implicit_reducible]

noncomputable instance MvPolynomial.decidableRestrictDegree (σ : Type u) (m : ℕ) : DecidablePred fun (x : σ →₀ ℕ) => x ∈ {n : σ →₀ ℕ | ∀ (i : σ), n i ≤ m}

theorem MvPolynomial.rank_R (σ K : Type u) [Fintype K] [Field K] [Fintype σ] : Module.rank K (R σ K) = ↑(Fintype.card (σ → K))

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

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

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

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

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