Mathlib.FieldTheory.Finite.Polynomial

Polynomials over finite fields #

source

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.

source

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

source

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

(MvPolynomial.expand p) f = f ^ p

source

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 = ∏ n : σ, (1 - (MvPolynomial.X n - MvPolynomial.C (a n)) ^ (Fintype.card K - 1))

Instances For

source

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

source

theorem MvPolynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (c : σ → K) :

(MvPolynomial.indicator c).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

source

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)

source

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

source

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 σ = { toFun := fun (p : MvPolynomial σ K) (e : σ → K) => (MvPolynomial.eval e) p, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[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

source

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)) = ⊤

source

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))

Instances For

source

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)))

source

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

Module K (MvPolynomial.R σ K)

Equations

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

source

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)))

source

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

MvPolynomial.R σ K →ₗ[K] (σ → K) → K

Evaluation in the MvPolynomial.R subtype.

Equations

MvPolynomial.evalᵢ σ K = MvPolynomial.evalₗ K σ ∘ₗ (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)).subtype

Instances For

source

noncomputable instance MvPolynomial.decidableRestrictDegree (σ : Type u) (m : ℕ) :

DecidablePred fun (x : σ →₀ ℕ) => x ∈ {n : σ →₀ ℕ | ∀ (i : σ), n i ≤ m}

Equations

MvPolynomial.decidableRestrictDegree σ m = id inferInstance

source

theorem MvPolynomial.rank_R (σ : Type u) (K : Type u) [Fintype K] [Field K] [Fintype σ] :

Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))

source

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

FiniteDimensional K (MvPolynomial.R σ K)

Equations

⋯ = ⋯

source

theorem MvPolynomial.finrank_R (σ : Type u) (K : Type u) [Fintype K] [Field K] [Fintype σ] :

Module.finrank K (MvPolynomial.R σ K) = Fintype.card (σ → K)

source

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

LinearMap.range (MvPolynomial.evalᵢ σ K) = ⊤

source

theorem MvPolynomial.ker_evalₗ (σ : Type u) (K : Type u) [Fintype K] [Field K] [Finite σ] :

LinearMap.ker (MvPolynomial.evalᵢ σ K) = ⊥

source

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