mathlib documentation

field_theory.mv_polynomial

def mv_polynomial.restrict_total_degree (σ : Type u) (α : Type v) [field α] :
submodule α (mv_polynomial σ α)

Equations
theorem mv_polynomial.mem_restrict_total_degree (σ : Type u) (α : Type v) [field α] (m : ) (p : mv_polynomial σ α) :

def mv_polynomial.restrict_degree (σ : Type u) (α : Type v) (m : ) [field α] :

Equations
theorem mv_polynomial.mem_restrict_degree {σ : Type u} {α : Type v} [field α] (p : mv_polynomial σ α) (n : ) :
p mv_polynomial.restrict_degree σ α n ∀ (s : σ →₀ ), s p.support∀ (i : σ), s i n

theorem mv_polynomial.mem_restrict_degree_iff_sup {σ : Type u} {α : Type v} [field α] (p : mv_polynomial σ α) (n : ) :

theorem mv_polynomial.map_range_eq_map {σ : Type u} {α : Type v} {β : Type u_1} [comm_ring α] [comm_ring β] (p : mv_polynomial σ α) (f : α →+* β) :

theorem mv_polynomial.is_basis_monomials (σ : Type u) (α : Type v) [field α] :

theorem mv_polynomial.dim_mv_polynomial (σ α : Type u) [field α] :

@[instance]
def mv_polynomial.char_p (σ : Type u_1) (R : Type u_2) [comm_ring R] (p : ) [char_p R p] :