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:

σ : 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

source

@[protected, instance]

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

comm_ring (mv_polynomial σ R)

Equations

mv_polynomial.comm_ring = add_monoid_algebra.comm_ring

source

@[simp]

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

⇑mv_polynomial.C (a - a') = ⇑mv_polynomial.C a - ⇑mv_polynomial.C a'

source

@[simp]

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

⇑mv_polynomial.C (-a) = -⇑mv_polynomial.C a

source

@[simp]

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

mv_polynomial.coeff m (-p) = -mv_polynomial.coeff m p

source

@[simp]

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

mv_polynomial.coeff m (p - q) = mv_polynomial.coeff m p - mv_polynomial.coeff m q

source

@[simp]

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

(-p).support = p.support

source

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

(p - q).support ⊆ p.support ∪ q.support

source

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

(-p).degrees = p.degrees

source

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

(p - q).degrees ≤ p.degrees ⊔ q.degrees

source

@[simp]

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

(-p).vars = p.vars

source

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

source

@[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

source

@[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) :

mv_polynomial.eval₂ f g (p - q) = mv_polynomial.eval₂ f g p - mv_polynomial.eval₂ f g q

source

@[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) :

mv_polynomial.eval₂ f g (-p) = -mv_polynomial.eval₂ f g p

source

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

⇑f (⇑mv_polynomial.C n) = ↑n

source

@[simp]

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

mv_polynomial.eval₂ c (⇑f ∘ mv_polynomial.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), ...

source

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

mv_polynomial.hom_equiv = {to_fun := λ (f : mv_polynomial σ ℤ →+* S), ⇑f ∘ mv_polynomial.X, inv_fun := λ (f : σ → S), mv_polynomial.eval₂_hom (int.cast_ring_hom S) f, left_inv := _, right_inv := _}

source

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) :

mv_polynomial.degree_of x (f - g) < k

source

@[simp]

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

(-a).total_degree = a.total_degree

source

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

(a - b).total_degree ≤ linear_order.max a.total_degree b.total_degree