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.

Equations

• MvPolynomial.indicator a = Finset.prod Finset.univ fun (n : σ) => 1 - (MvPolynomial.X n - MvPolynomial.C (a n)) ^ (Fintype.card K - 1)

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.

Equations

• MvPolynomial.evalₗ K σ = { toAddHom := { toFun := fun (p : MvPolynomial σ K) (e : σ → K) => (MvPolynomial.eval e) p, map_add' := ⋯ }, map_smul' := ⋯ }

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.

Equations

• MvPolynomial.R σ K = ↥(MvPolynomial.restrictDegree σ K (Fintype.card K - 1))

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

Equations

• MvPolynomial.instAddCommGroupR σ K = inferInstanceAs (AddCommGroup ↥(MvPolynomial.restrictDegree σ K (Fintype.card K - 1)))

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

Equations

• MvPolynomial.instModuleRToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupR σ K = inferInstanceAs (Module K ↥(MvPolynomial.restrictDegree σ K (Fintype.card K - 1)))

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

Equations

• MvPolynomial.instInhabitedR σ K = inferInstanceAs (Inhabited ↥(MvPolynomial.restrictDegree σ K (Fintype.card K - 1)))

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.

Equations

• MvPolynomial.evalᵢ σ K = LinearMap.comp (MvPolynomial.evalₗ K σ) (Submodule.subtype (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)))

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

Equations

• MvPolynomial.decidableRestrictDegree σ m = id inferInstance

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)

Equations

• ⋯ = ⋯

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