def
mv_polynomial.restrict_total_degree
(σ : Type u)
(α : Type v)
[field α] :
ℕ → submodule α (mv_polynomial σ α)
Equations
- mv_polynomial.restrict_total_degree σ α m = finsupp.supported α α {n : σ →₀ ℕ | n.sum (λ (n : σ) (e : ℕ), e) ≤ m}
theorem
mv_polynomial.mem_restrict_total_degree
(σ : Type u)
(α : Type v)
[field α]
(m : ℕ)
(p : mv_polynomial σ α) :
p ∈ mv_polynomial.restrict_total_degree σ α m ↔ p.total_degree ≤ m
def
mv_polynomial.restrict_degree
(σ : Type u)
(α : Type v)
(m : ℕ)
[field α] :
submodule α (mv_polynomial σ α)
Equations
- mv_polynomial.restrict_degree σ α m = finsupp.supported α α {n : σ →₀ ℕ | ∀ (i : σ), ⇑n i ≤ m}
theorem
mv_polynomial.mem_restrict_degree
{σ : Type u}
{α : Type v}
[field α]
(p : mv_polynomial σ α)
(n : ℕ) :
theorem
mv_polynomial.mem_restrict_degree_iff_sup
{σ : Type u}
{α : Type v}
[field α]
(p : mv_polynomial σ α)
(n : ℕ) :
p ∈ mv_polynomial.restrict_degree σ α n ↔ ∀ (i : σ), multiset.count i p.degrees ≤ n
theorem
mv_polynomial.map_range_eq_map
{σ : Type u}
{α : Type v}
{β : Type u_1}
[comm_ring α]
[comm_ring β]
(p : mv_polynomial σ α)
(f : α →+* β) :
finsupp.map_range ⇑f _ p = ⇑(mv_polynomial.map f) p
theorem
mv_polynomial.is_basis_monomials
(σ : Type u)
(α : Type v)
[field α] :
is_basis α (λ (s : σ →₀ ℕ), mv_polynomial.monomial s 1)
theorem
mv_polynomial.dim_mv_polynomial
(σ α : Type u)
[field α] :
vector_space.dim α (mv_polynomial σ α) = cardinal.mk (σ →₀ ℕ)
def
mv_polynomial.indicator
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ] :
(σ → α) → mv_polynomial σ α
Equations
- mv_polynomial.indicator a = finset.univ.prod (λ (n : σ), 1 - (mv_polynomial.X n - ⇑mv_polynomial.C (a n)) ^ (fintype.card α - 1))
theorem
mv_polynomial.eval_indicator_apply_eq_one
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ]
(a : σ → α) :
⇑(mv_polynomial.eval a) (mv_polynomial.indicator a) = 1
theorem
mv_polynomial.eval_indicator_apply_eq_zero
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ]
(a b : σ → α) :
a ≠ b → ⇑(mv_polynomial.eval a) (mv_polynomial.indicator b) = 0
theorem
mv_polynomial.degrees_indicator
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ]
(c : σ → α) :
(mv_polynomial.indicator c).degrees ≤ finset.univ.sum (λ (s : σ), (fintype.card α - 1) •ℕ {s})
theorem
mv_polynomial.indicator_mem_restrict_degree
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ]
(c : σ → α) :
def
mv_polynomial.evalₗ
(α : Type u_1)
(σ : Type u_2)
[field α]
[fintype α]
[fintype σ] :
mv_polynomial σ α →ₗ[α] (σ → α) → α
Equations
- mv_polynomial.evalₗ α σ = {to_fun := λ (p : mv_polynomial σ α) (e : σ → α), ⇑(mv_polynomial.eval e) p, map_add' := _, map_smul' := _}
theorem
mv_polynomial.evalₗ_apply
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ]
(p : mv_polynomial σ α)
(e : σ → α) :
⇑(mv_polynomial.evalₗ α σ) p e = ⇑(mv_polynomial.eval e) p
theorem
mv_polynomial.map_restrict_dom_evalₗ
{α : Type u_1}
{σ : Type u_2}
[field α]
[fintype α]
[fintype σ] :
submodule.map (mv_polynomial.evalₗ α σ) (mv_polynomial.restrict_degree σ α (fintype.card α - 1)) = ⊤
@[instance]
def
mv_polynomial.R.inst
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
vector_space α (mv_polynomial.R σ α)
@[instance]
@[instance]
def
mv_polynomial.R.inhabited
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
inhabited (mv_polynomial.R σ α)
Equations
- mv_polynomial.R σ α = ↥(mv_polynomial.restrict_degree σ α (fintype.card α - 1))
@[instance]
Equations
- mv_polynomial.decidable_restrict_degree σ m = _.mpr (λ (a : σ →₀ ℕ), fintype.decidable_forall_fintype)
theorem
mv_polynomial.dim_R
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
vector_space.dim α (mv_polynomial.R σ α) = ↑(fintype.card (σ → α))
def
mv_polynomial.evalᵢ
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
mv_polynomial.R σ α →ₗ[α] (σ → α) → α
Equations
- mv_polynomial.evalᵢ σ α = (mv_polynomial.evalₗ α σ).comp (mv_polynomial.restrict_degree σ α (fintype.card α - 1)).subtype
theorem
mv_polynomial.range_evalᵢ
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
(mv_polynomial.evalᵢ σ α).range = ⊤
theorem
mv_polynomial.ker_evalₗ
(σ α : Type u)
[fintype σ]
[field α]
[fintype α] :
(mv_polynomial.evalᵢ σ α).ker = ⊥
theorem
mv_polynomial.eq_zero_of_eval_eq_zero
(σ α : Type u)
[fintype σ]
[field α]
[fintype α]
(p : mv_polynomial σ α) :
(∀ (v : σ → α), ⇑(mv_polynomial.eval v) p = 0) → p ∈ mv_polynomial.restrict_degree σ α (fintype.card α - 1) → p = 0
@[instance]
def
mv_polynomial.char_p
(σ : Type u_1)
(R : Type u_2)
[comm_ring R]
(p : ℕ)
[char_p R p] :
char_p (mv_polynomial σ R) p
Equations
- _ = _