# mathlibdocumentation

data.mv_polynomial.comm_ring

# Multivariate polynomials over a ring

Many results about polynomials hold when the coefficient ring is a commutative semiring. Some stronger results can be derived when we assume this semiring is a ring.

This file does not define any new operations, but proves some of these stronger results.

## Notation

As in other polynomial files, we typically use the notation:

• σ : Type* (indexing the variables)

• R : Type* [comm_ring R] (the coefficients)

• s : σ →₀ ℕ, a function from σ to ℕ which is zero away from a finite set. This will give rise to a monomial in mv_polynomial σ R which mathematicians might call X^s

• a : R

• i : σ, with corresponding monomial X i, often denoted X_i by mathematicians

• p : mv_polynomial σ R

@[instance]
def mv_polynomial.comm_ring {R : Type u} {σ : Type u_1} [comm_ring R] :

Equations
@[instance]
def mv_polynomial.C.is_ring_hom {R : Type u} {σ : Type u_1} [comm_ring R] :

@[simp]
theorem mv_polynomial.C_sub {R : Type u} (σ : Type u_1) (a a' : R) [comm_ring R] :

@[simp]
theorem mv_polynomial.C_neg {R : Type u} (σ : Type u_1) (a : R) [comm_ring R] :

@[simp]
theorem mv_polynomial.coeff_neg {R : Type u} (σ : Type u_1) [comm_ring R] (m : σ →₀ ) (p : R) :

@[simp]
theorem mv_polynomial.coeff_sub {R : Type u} (σ : Type u_1) [comm_ring R] (m : σ →₀ ) (p q : R) :
(p - q) =

@[instance]
def mv_polynomial.coeff.is_add_group_hom {R : Type u} (σ : Type u_1) [comm_ring R] (m : σ →₀ ) :

theorem mv_polynomial.degrees_neg {R : Type u} {σ : Type u_1} [comm_ring R] (p : R) :

theorem mv_polynomial.degrees_sub {R : Type u} {σ : Type u_1} [comm_ring R] (p q : R) :

@[simp]
theorem mv_polynomial.vars_neg {R : Type u} {σ : Type u_1} [comm_ring R] (p : R) :
(-p).vars = p.vars

theorem mv_polynomial.vars_sub_subset {R : Type u} {σ : Type u_1} [comm_ring R] (p q : R) :
(p - q).vars p.vars q.vars

@[simp]
theorem mv_polynomial.vars_sub_of_disjoint {R : Type u} {σ : Type u_1} [comm_ring R] {p q : R} :
q.vars(p - q).vars = p.vars q.vars

@[simp]
theorem mv_polynomial.eval₂_sub {R : Type u} {S : Type v} {σ : Type u_1} [comm_ring R] (p : R) {q : R} [comm_ring S] (f : R →+* S) (g : σ → S) :
(p - q) = p - q

@[simp]
theorem mv_polynomial.eval₂_neg {R : Type u} {S : Type v} {σ : Type u_1} [comm_ring R] (p : R) [comm_ring S] (f : R →+* S) (g : σ → S) :
(-p) = - p

theorem mv_polynomial.hom_C {S : Type v} {σ : Type u_1} [comm_ring S] (f : → S) [is_ring_hom f] (n : ) :
f = n

@[simp]
theorem mv_polynomial.eval₂_hom_X {S : Type v} [comm_ring S] {R : Type u} (c : →+* S) (f : →+* S) (x : ) :
x = f x

A ring homomorphism f : Z[X_1, X_2, ...] → R is determined by the evaluations f(X_1), f(X_2), ...

def mv_polynomial.hom_equiv {S : Type v} {σ : Type u_1} [comm_ring S] :
→+* S) (σ → S)

Ring homomorphisms out of integer polynomials on a type σ are the same as functions out of the type σ,

Equations
@[simp]
theorem mv_polynomial.total_degree_neg {R : Type u} {σ : Type u_1} [comm_ring R] (a : R) :

theorem mv_polynomial.total_degree_sub {R : Type u} {σ : Type u_1} [comm_ring R] (a b : R) :