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
.
Instances For
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.
Instances For
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)) = ⊤
noncomputable instance
MvPolynomial.instAddCommGroupR
(σ : Type u)
(K : Type u)
[Fintype K]
[CommRing K]
:
AddCommGroup (MvPolynomial.R σ K)
noncomputable instance
MvPolynomial.instModuleRToSemiringToCommSemiringToAddCommMonoidInstAddCommGroupR
(σ : Type u)
(K : Type u)
[Fintype K]
[CommRing K]
:
Module K (MvPolynomial.R σ K)
noncomputable instance
MvPolynomial.instInhabitedR
(σ : Type u)
(K : Type u)
[Fintype K]
[CommRing K]
:
Inhabited (MvPolynomial.R σ K)
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.
Instances For
noncomputable instance
MvPolynomial.decidableRestrictDegree
(σ : Type u)
(m : ℕ)
:
DecidablePred fun x => x ∈ {n | ∀ (i : σ), ↑n i ≤ m}
theorem
MvPolynomial.rank_R
(σ : Type u)
(K : Type u)
[Fintype K]
[Field K]
[Fintype σ]
:
Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))
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