# Documentation

Mathlib.Data.MvPolynomial.CommRing

# 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* [CommRing R] (the coefficients)

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

• a : R

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

• p : MvPolynomial σ R

theorem MvPolynomial.C_sub {R : Type u} (σ : Type u_1) (a : R) (a' : R) [] :
MvPolynomial.C (a - a') = MvPolynomial.C a - MvPolynomial.C a'
theorem MvPolynomial.C_neg {R : Type u} (σ : Type u_1) (a : R) [] :
MvPolynomial.C (-a) = -MvPolynomial.C a
@[simp]
theorem MvPolynomial.coeff_neg {R : Type u} (σ : Type u_1) [] (m : σ →₀ ) (p : ) :
=
@[simp]
theorem MvPolynomial.coeff_sub {R : Type u} (σ : Type u_1) [] (m : σ →₀ ) (p : ) (q : ) :
@[simp]
theorem MvPolynomial.support_neg {R : Type u} (σ : Type u_1) [] {p : } :
theorem MvPolynomial.support_sub {R : Type u} (σ : Type u_1) [] [] (p : ) (q : ) :
theorem MvPolynomial.degrees_neg {R : Type u} {σ : Type u_1} [] (p : ) :
theorem MvPolynomial.degrees_sub {R : Type u} {σ : Type u_1} [] [] (p : ) (q : ) :
@[simp]
theorem MvPolynomial.vars_neg {R : Type u} {σ : Type u_1} [] (p : ) :
theorem MvPolynomial.vars_sub_subset {R : Type u} {σ : Type u_1} [] (p : ) {q : } [] :
@[simp]
theorem MvPolynomial.vars_sub_of_disjoint {R : Type u} {σ : Type u_1} [] (p : ) {q : } [] (hpq : ) :
@[simp]
theorem MvPolynomial.eval₂_sub {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) {q : } [] (f : R →+* S) (g : σS) :
theorem MvPolynomial.eval_sub {R : Type u} {σ : Type u_1} [] (p : ) {q : } (f : σR) :
↑() (p - q) = ↑() p - ↑() q
@[simp]
theorem MvPolynomial.eval₂_neg {R : Type u} {S : Type v} {σ : Type u_1} [] (p : ) [] (f : R →+* S) (g : σS) :
theorem MvPolynomial.eval_neg {R : Type u} {σ : Type u_1} [] (p : ) (f : σR) :
↑() (-p) = -↑() p
theorem MvPolynomial.hom_C {S : Type v} {σ : Type u_1} [] (f : →+* S) (n : ) :
f (MvPolynomial.C n) = n
@[simp]
theorem MvPolynomial.eval₂Hom_X {S : Type v} [] {R : Type u} (c : →+* S) (f : →+* S) (x : ) :
MvPolynomial.eval₂ c (f MvPolynomial.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 MvPolynomial.homEquiv {S : Type v} {σ : Type u_1} [] :
( →+* S) (σS)

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

Instances For
theorem MvPolynomial.degreeOf_sub_lt {R : Type u} {σ : Type u_1} [] {x : σ} {f : } {g : } {k : } (h : 0 < k) (hf : ∀ (m : σ →₀ ), k m x) (hg : ∀ (m : σ →₀ ), k m x) :
@[simp]
theorem MvPolynomial.totalDegree_neg {R : Type u} {σ : Type u_1} [] (a : ) :
theorem MvPolynomial.totalDegree_sub {R : Type u} {σ : Type u_1} [] (a : ) (b : ) :