mathlib3 documentation


Polynomials over finite fields #

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

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

theorem mv_polynomial.expand_zmod {σ : Type u_1} {p : } [fact ( p)] (f : mv_polynomial σ (zmod p)) :
noncomputable def mv_polynomial.indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (a : σ K) :

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

theorem mv_polynomial.degrees_indicator {K : Type u_1} {σ : Type u_2} [fintype K] [fintype σ] [comm_ring K] (c : σ K) :
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) :
theorem mv_polynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) [comm_semiring K] (p : mv_polynomial σ K) (e : σ K) :
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.

@[protected, instance]
noncomputable def mv_polynomial.R.add_comm_group (σ K : Type u) [fintype K] [comm_ring K] :
@[protected, instance]
noncomputable def mv_polynomial.R.inhabited (σ K : Type u) [fintype K] [comm_ring K] :
def mv_polynomial.R (σ K : Type u) [fintype K] [comm_ring K] :

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

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

Evaluation in the mv_polynomial.R subtype.

@[protected, instance]
noncomputable def mv_polynomial.decidable_restrict_degree (σ : Type u) (m : ) :
decidable_pred (λ (_x : σ →₀ ), _x {n : σ →₀ | (i : σ), n i m})
theorem mv_polynomial.rank_R (σ K : Type u) [fintype K] [field K] [fintype σ] :
@[protected, instance]
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