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:

Equations
  • MvPolynomial.instCommRingMvPolynomial = AddMonoidAlgebra.commRing
theorem MvPolynomial.C_sub {R : Type u} (σ : Type u_1) (a : R) (a' : R) [CommRing R] :
MvPolynomial.C (a - a') = MvPolynomial.C a - MvPolynomial.C a'
theorem MvPolynomial.C_neg {R : Type u} (σ : Type u_1) (a : R) [CommRing R] :
MvPolynomial.C (-a) = -MvPolynomial.C a
@[simp]
theorem MvPolynomial.coeff_neg {R : Type u} (σ : Type u_1) [CommRing R] (m : σ →₀ ) (p : MvPolynomial σ R) :
@[simp]
theorem MvPolynomial.coeff_sub {R : Type u} (σ : Type u_1) [CommRing R] (m : σ →₀ ) (p : MvPolynomial σ R) (q : MvPolynomial σ R) :
@[simp]
@[simp]
theorem MvPolynomial.eval₂_sub {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} [CommRing S] (f : R →+* S) (g : σS) :
theorem MvPolynomial.eval_sub {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) {q : MvPolynomial σ R} (f : σR) :
@[simp]
theorem MvPolynomial.eval₂_neg {R : Type u} {S : Type v} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) [CommRing S] (f : R →+* S) (g : σS) :
theorem MvPolynomial.eval_neg {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) (f : σR) :
theorem MvPolynomial.hom_C {S : Type v} {σ : Type u_1} [CommRing S] (f : MvPolynomial σ →+* S) (n : ) :
f (MvPolynomial.C n) = n
@[simp]
theorem MvPolynomial.eval₂Hom_X {S : Type v} [CommRing S] {R : Type u} (c : →+* S) (f : MvPolynomial R →+* S) (x : MvPolynomial R ) :
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} [CommRing S] :
(MvPolynomial σ →+* S) (σS)

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem MvPolynomial.degreeOf_sub_lt {R : Type u} {σ : Type u_1} [CommRing R] {x : σ} {f : MvPolynomial σ R} {g : MvPolynomial σ R} {k : } (h : 0 < k) (hf : mMvPolynomial.support f, k m xMvPolynomial.coeff m f = MvPolynomial.coeff m g) (hg : mMvPolynomial.support g, k m xMvPolynomial.coeff m f = MvPolynomial.coeff m g) :
    theorem MvPolynomial.totalDegree_sub_C_le {R : Type u} {σ : Type u_1} [CommRing R] (p : MvPolynomial σ R) (r : R) :