mathlib3 documentation

data.mv_polynomial.comm_ring

Multivariate polynomials over a ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

@[protected, instance]
noncomputable def mv_polynomial.comm_ring {R : Type u} {σ : Type u_1} [comm_ring R] :
Equations
@[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 : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.coeff_sub {R : Type u} (σ : Type u_1) [comm_ring R] (m : σ →₀ ) (p q : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.support_neg {R : Type u} (σ : Type u_1) [comm_ring R] {p : mv_polynomial σ R} :
theorem mv_polynomial.support_sub {R : Type u} (σ : Type u_1) [comm_ring R] [decidable_eq σ] (p q : mv_polynomial σ R) :
theorem mv_polynomial.degrees_neg {R : Type u} {σ : Type u_1} [comm_ring R] (p : mv_polynomial σ R) :
theorem mv_polynomial.degrees_sub {R : Type u} {σ : Type u_1} [comm_ring R] [decidable_eq σ] (p q : mv_polynomial σ R) :
@[simp]
theorem mv_polynomial.vars_neg {R : Type u} {σ : Type u_1} [comm_ring R] (p : mv_polynomial σ R) :
(-p).vars = p.vars
theorem mv_polynomial.vars_sub_subset {R : Type u} {σ : Type u_1} [comm_ring R] (p q : mv_polynomial σ R) [decidable_eq σ] :
(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 : mv_polynomial σ R} [decidable_eq σ] (hpq : disjoint p.vars 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 : mv_polynomial σ R) {q : mv_polynomial σ R} [comm_ring S] (f : R →+* S) (g : σ S) :
@[simp]
theorem mv_polynomial.eval₂_neg {R : Type u} {S : Type v} {σ : Type u_1} [comm_ring R] (p : mv_polynomial σ R) [comm_ring S] (f : R →+* S) (g : σ S) :
theorem mv_polynomial.hom_C {S : Type v} {σ : Type u_1} [comm_ring S] (f : mv_polynomial σ →+* S) (n : ) :
@[simp]

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

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

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

Equations
theorem mv_polynomial.degree_of_sub_lt {R : Type u} {σ : Type u_1} [comm_ring R] {x : σ} {f g : mv_polynomial σ R} {k : } (h : 0 < k) (hf : (m : σ →₀ ), m f.support k m x mv_polynomial.coeff m f = mv_polynomial.coeff m g) (hg : (m : σ →₀ ), m g.support k m x mv_polynomial.coeff m f = mv_polynomial.coeff m g) :
@[simp]
theorem mv_polynomial.total_degree_neg {R : Type u} {σ : Type u_1} [comm_ring R] (a : mv_polynomial σ R) :