Documentation

Mathlib.FieldTheory.Finite.Polynomial

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)) :
theorem MvPolynomial.expand_zmod {σ : Type u_1} {p : } [Fact (Nat.Prime p)] (f : MvPolynomial σ (ZMod p)) :
def MvPolynomial.indicator {K : Type u_1} {σ : Type u_2} [Fintype K] [Fintype σ] [CommRing K] (a : σK) :

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

Equations
Instances For
    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}
    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) :
    @[simp]
    theorem MvPolynomial.evalₗ_apply (K : Type u_1) (σ : Type u_2) [CommSemiring K] (p : MvPolynomial σ K) (e : σK) :
    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
    Instances For
      def MvPolynomial.R (σ : Type u) (K : Type u) [Fintype K] [CommRing K] :

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

      Equations
      Instances For
        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
        Instances For
          noncomputable instance MvPolynomial.decidableRestrictDegree (σ : Type u) (m : ) :
          DecidablePred fun (x : σ →₀ ) => x {n : σ →₀ | ∀ (i : σ), n i m}
          Equations
          theorem MvPolynomial.rank_R (σ : Type u) (K : Type u) [Fintype K] [Field K] [Fintype σ] :
          Module.rank K (MvPolynomial.R σ K) = (Fintype.card (σK))
          Equations
          • =
          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