mathlib3 documentation

field_theory.finite.polynomial

Polynomials over finite fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem mv_polynomial.C_dvd_iff_zmod {σ : Type u_1} (n : ℕ) (φ : mv_polynomial σ ℤ) :
⇑mv_polynomial.C ↑n ∣ φ ↔ ⇑(mv_polynomial.map (int.cast_ring_hom (zmod n))) φ = 0

A polynomial over the integers is divisible by n : ℕ if and only if it is zero over zmod n.

source
theorem mv_polynomial.frobenius_zmod {σ : Type u_1} {p : ℕ} [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
⇑(frobenius (mv_polynomial σ (zmod p)) p) f = ⇑(mv_polynomial.expand p) f
source
theorem mv_polynomial.expand_zmod {σ : Type u_1} {p : ℕ} [fact (nat.prime p)] (f : mv_polynomial σ (zmod p)) :
⇑(mv_polynomial.expand p) f = f ^ p
source
noncomputable def mv_polynomial.indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (a : σ → K) :
mv_polynomial σ K

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

Equations
source
theorem mv_polynomial.eval_indicator_apply_eq_one {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (a : σ → K) :
⇑(mv_polynomial.eval a) (mv_polynomial.indicator a) = 1
source
theorem mv_polynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (c : σ → K) :
(mv_polynomial.indicator c).degrees ≤ finset.univ.sum (λ (s : σ), (fintype.card K - 1) • {s})
source
theorem mv_polynomial.indicator_mem_restrict_degree {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (c : σ → K) :
mv_polynomial.indicator c ∈ mv_polynomial.restrict_degree σ K (fintype.card K - 1)
source
theorem mv_polynomial.eval_indicator_apply_eq_zero {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [field K] (a b : σ → K) (h : a ≠ b) :
⇑(mv_polynomial.eval a) (mv_polynomial.indicator b) = 0
source
@[simp]
theorem mv_polynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) [comm_semiring K] (p : mv_polynomial σ K) (e : σ → K) :
⇑(mv_polynomial.evalₗ K σ) p e = ⇑(mv_polynomial.eval e) p
source
noncomputable def mv_polynomial.evalₗ (K : Type u_1) (σ : Type u_2) [comm_semiring K] :
mv_polynomial σ K →ₗ[K] (σ → K) → K

mv_polynomial.eval as a K-linear map.

Equations
source
theorem mv_polynomial.map_restrict_dom_evalₗ {K : Type u_1} {σ : Type u_2} [field K] [fintype K] [finite σ] :
submodule.map (mv_polynomial.evalₗ K σ) (mv_polynomial.restrict_degree σ K (fintype.card K - 1)) = ⊤
source
@[protected, instance]
noncomputable def mv_polynomial.R.add_comm_group (σ K : Type u) [fintype K] [comm_ring K] :
add_comm_group (mv_polynomial.R σ K)
source
@[protected, instance]
noncomputable def mv_polynomial.R.inhabited (σ K : Type u) [fintype K] [comm_ring K] :
inhabited (mv_polynomial.R σ K)
source
def mv_polynomial.R (σ K : Type u) [fintype K] [comm_ring K] :
Type u

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

Equations
Instances for mv_polynomial.R
source
@[protected, instance]
noncomputable def mv_polynomial.R.module (σ K : Type u) [fintype K] [comm_ring K] :
module K (mv_polynomial.R σ K)
source
noncomputable def mv_polynomial.evalᵢ (σ K : Type u) [fintype K] [comm_ring K] :
mv_polynomial.R σ K →ₗ[K] (σ → K) → K

Evaluation in the mv_polynomial.R subtype.

Equations
source
@[protected, instance]
noncomputable def mv_polynomial.decidable_restrict_degree (σ : Type u) (m : ℕ) :
decidable_pred (λ (_x : σ →₀ ℕ), _x ∈ {n : σ →₀ ℕ | ∀ (i : σ), ⇑n i ≤ m})
Equations
source
theorem mv_polynomial.rank_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
module.rank K (mv_polynomial.R σ K) = ↑(fintype.card (σ → K))
source
@[protected, instance]
def mv_polynomial.R.finite_dimensional (σ K : Type u) [fintype K] [field K] [finite σ] :
finite_dimensional K (mv_polynomial.R σ K)
source
theorem mv_polynomial.finrank_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
finite_dimensional.finrank K (mv_polynomial.R σ K) = fintype.card (σ → K)
source
theorem mv_polynomial.range_evalᵢ (σ K : Type u) [fintype K] [field K] [finite σ] :
linear_map.range (mv_polynomial.evalᵢ σ K) = ⊤
source
theorem mv_polynomial.ker_evalₗ (σ K : Type u) [fintype K] [field K] [finite σ] :
linear_map.ker (mv_polynomial.evalᵢ σ K) = ⊥
source
theorem mv_polynomial.eq_zero_of_eval_eq_zero (σ K : Type u) [fintype K] [field K] [finite σ] (p : mv_polynomial σ K) (h : ∀ (v : σ → K), ⇑(mv_polynomial.eval v) p = 0) (hp : p ∈ mv_polynomial.restrict_degree σ K (fintype.card K - 1)) :
p = 0