def
mv_polynomial.restrict_total_degree
(σ : Type u)
(α : Type v)
[field α]
(m : ℕ) :
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 σ α) = # (σ →₀ ℕ)
@[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