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
.
Equations
- MvPolynomial.indicator a = ∏ n : σ, (1 - (MvPolynomial.X n - MvPolynomial.C (a n)) ^ (Fintype.card K - 1))
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.indicator c).degrees ≤ ∑ 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.
Equations
- MvPolynomial.evalₗ K σ = { toFun := fun (p : MvPolynomial σ K) (e : σ → K) => (MvPolynomial.eval e) p, map_add' := ⋯, map_smul' := ⋯ }
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)) = ⊤
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
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)))
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)))
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)))
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
Equations
- MvPolynomial.decidableRestrictDegree σ m = id inferInstance
theorem
MvPolynomial.rank_R
(σ : Type u)
(K : Type u)
[Fintype K]
[Field K]
[Fintype σ]
:
Module.rank K (MvPolynomial.R σ K) = ↑(Fintype.card (σ → K))
instance
MvPolynomial.instFiniteDimensionalROfFinite
(σ : Type u)
(K : Type u)
[Fintype K]
[Field K]
[Finite σ]
:
FiniteDimensional K (MvPolynomial.R σ K)
Equations
- ⋯ = ⋯
theorem
MvPolynomial.finrank_R
(σ : Type u)
(K : Type u)
[Fintype K]
[Field K]
[Fintype σ]
:
Module.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