mathlib documentation

data.polynomial.basic

Theory of univariate polynomials #

This file defines polynomial R, the type of univariate polynomials over the semiring R, builds a semiring structure on it, and gives basic definitions that are expanded in other files in this directory.

Main definitions #

There are often two natural variants of lemmas involving sums, depending on whether one acts on the polynomials, or on the function. The naming convention is that one adds index when acting on the polynomials. For instance,

Implementation #

Polynomials are defined using add_monoid_algebra R ℕ, where R is a commutative semiring, but through a structure to make them irreducible from the point of view of the kernel. Most operations are irreducible since Lean can not compute anyway with add_monoid_algebra. There are two exceptions that we make semireducible:

The raw implementation of the equivalence between polynomial R and add_monoid_algebra R ℕ is done through of_finsupp and to_finsupp (or, equivalently, rcases p when p is a polynomial gives an element q of add_monoid_algebra R ℕ, and conversely ⟨q⟩ gives back p). The equivalence is also registered as a ring equiv in polynomial.to_finsupp_iso. These should in general not be used once the basic API for polynomials is constructed.

structure polynomial (R : Type u_1) [semiring R] :
Type u_1

polynomial R is the type of univariate polynomials over R.

Polynomials should be seen as (semi-)rings with the additional constructor X. The embedding from R is called C.

theorem polynomial.forall_iff_forall_finsupp {R : Type u} [semiring R] (P : polynomial R → Prop) :
(∀ (p : polynomial R), P p) ∀ (q : add_monoid_algebra R ), P {to_finsupp := q}
theorem polynomial.exists_iff_exists_finsupp {R : Type u} [semiring R] (P : polynomial R → Prop) :
(∃ (p : polynomial R), P p) ∃ (q : add_monoid_algebra R ), P {to_finsupp := q}
def polynomial.monomial_fun {R : Type u} [semiring R] (n : ) (a : R) :

The function version of monomial. Use monomial instead of this one.

Equations
@[instance]
def polynomial.has_zero {R : Type u} [semiring R] :
Equations
@[instance]
def polynomial.has_one {R : Type u} [semiring R] :
Equations
@[instance]
def polynomial.has_add {R : Type u} [semiring R] :
Equations
@[instance]
def polynomial.has_neg {R : Type u} [ring R] :
Equations
@[instance]
def polynomial.has_mul {R : Type u} [semiring R] :
Equations
@[instance]
def polynomial.has_scalar {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] :
Equations
theorem polynomial.zero_to_finsupp {R : Type u} [semiring R] :
{to_finsupp := 0} = 0
theorem polynomial.one_to_finsupp {R : Type u} [semiring R] :
{to_finsupp := 1} = 1
theorem polynomial.add_to_finsupp {R : Type u} [semiring R] {a b : add_monoid_algebra R } :
{to_finsupp := a} + {to_finsupp := b} = {to_finsupp := a + b}
theorem polynomial.neg_to_finsupp {R : Type u} [ring R] {a : add_monoid_algebra R } :
-{to_finsupp := a} = {to_finsupp := -a}
theorem polynomial.mul_to_finsupp {R : Type u} [semiring R] {a b : add_monoid_algebra R } :
{to_finsupp := a} * {to_finsupp := b} = {to_finsupp := a * b}
theorem polynomial.smul_to_finsupp {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] {a : S} {b : add_monoid_algebra R } :
a {to_finsupp := b} = {to_finsupp := a b}
@[instance]
def polynomial.inhabited {R : Type u} [semiring R] :
Equations
@[instance]
def polynomial.module {R : Type u} [semiring R] {S : Type u_1} [semiring S] [module S R] :
Equations
@[instance]
def polynomial.smul_comm_class {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [monoid S₁] [monoid S₂] [distrib_mul_action S₁ R] [distrib_mul_action S₂ R] [smul_comm_class S₁ S₂ R] :
@[instance]
def polynomial.is_scalar_tower {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [has_scalar S₁ S₂] [monoid S₁] [monoid S₂] [distrib_mul_action S₁ R] [distrib_mul_action S₂ R] [is_scalar_tower S₁ S₂ R] :

Ring isomorphism between polynomial R and add_monoid_algebra R ℕ. This is just an implementation detail, but it can be useful to transfer results from finsupp to polynomials.

Equations
theorem polynomial.sum_to_finsupp {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → add_monoid_algebra R ) :
∑ (i : ι) in s, {to_finsupp := f i} = {to_finsupp := ∑ (i : ι) in s, f i}
def polynomial.support {R : Type u} [semiring R] :

The set of all n such that X^n has a non-zero coefficient.

Equations
@[simp]
theorem polynomial.support_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.support_eq_empty {R : Type u} [semiring R] {p : polynomial R} :
p.support = p = 0
theorem polynomial.card_support_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.support.card = 0 p = 0
def polynomial.monomial {R : Type u} [semiring R] (n : ) :

monomial s a is the monomial a * X^s

Equations
@[simp]
theorem polynomial.monomial_zero_right {R : Type u} [semiring R] (n : ) :
theorem polynomial.monomial_add {R : Type u} [semiring R] (n : ) (r s : R) :
theorem polynomial.monomial_mul_monomial {R : Type u} [semiring R] (n m : ) (r s : R) :
@[simp]
theorem polynomial.monomial_pow {R : Type u} [semiring R] (n : ) (r : R) (k : ) :
theorem polynomial.smul_monomial {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] (a : S) (n : ) (b : R) :
theorem polynomial.support_add {R : Type u} [semiring R] {p q : polynomial R} :
def polynomial.C {R : Type u} [semiring R] :

C a is the constant polynomial a. C is provided as a ring homomorphism.

Equations
@[simp]
theorem polynomial.monomial_zero_left {R : Type u} [semiring R] (a : R) :
theorem polynomial.C_0 {R : Type u} [semiring R] :
theorem polynomial.C_1 {R : Type u} [semiring R] :
theorem polynomial.C_mul {R : Type u} {a b : R} [semiring R] :
theorem polynomial.C_add {R : Type u} {a b : R} [semiring R] :
@[simp]
theorem polynomial.smul_C {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] (s : S) (r : R) :
@[simp]
theorem polynomial.C_bit0 {R : Type u} {a : R} [semiring R] :
@[simp]
theorem polynomial.C_bit1 {R : Type u} {a : R} [semiring R] :
theorem polynomial.C_pow {R : Type u} {a : R} {n : } [semiring R] :
@[simp]
theorem polynomial.C_eq_nat_cast {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.C_mul_monomial {R : Type u} {a b : R} {n : } [semiring R] :
@[simp]
theorem polynomial.monomial_mul_C {R : Type u} {a b : R} {n : } [semiring R] :
def polynomial.X {R : Type u} [semiring R] :

X is the polynomial variable (aka indeterminate).

Equations
theorem polynomial.X_mul {R : Type u} [semiring R] {p : polynomial R} :

X commutes with everything, even when the coefficients are noncommutative.

theorem polynomial.X_pow_mul {R : Type u} [semiring R] {p : polynomial R} {n : } :
theorem polynomial.X_pow_mul_assoc {R : Type u} [semiring R] {p q : polynomial R} {n : } :
(p * polynomial.X ^ n) * q = (p * q) * polynomial.X ^ n
theorem polynomial.commute_X {R : Type u} [semiring R] (p : polynomial R) :
@[simp]
theorem polynomial.monomial_mul_X {R : Type u} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.monomial_mul_X_pow {R : Type u} [semiring R] (n : ) (r : R) (k : ) :
@[simp]
theorem polynomial.X_mul_monomial {R : Type u} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.X_pow_mul_monomial {R : Type u} [semiring R] (k n : ) (r : R) :
def polynomial.coeff {R : Type u} [semiring R] :
polynomial R → R

coeff p n (often denoted p.coeff n) is the coefficient of X^n in p.

Equations
theorem polynomial.coeff_monomial {R : Type u} {a : R} {m n : } [semiring R] :
((polynomial.monomial n) a).coeff m = ite (n = m) a 0
@[simp]
theorem polynomial.coeff_zero {R : Type u} [semiring R] (n : ) :
0.coeff n = 0
@[simp]
theorem polynomial.coeff_one_zero {R : Type u} [semiring R] :
1.coeff 0 = 1
@[simp]
theorem polynomial.coeff_X_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.coeff_X_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : } [semiring R] :
theorem polynomial.coeff_X {R : Type u} {n : } [semiring R] :
polynomial.X.coeff n = ite (1 = n) 1 0
theorem polynomial.coeff_X_of_ne_one {R : Type u} [semiring R] {n : } (hn : n 1) :
@[simp]
theorem polynomial.mem_support_iff {R : Type u} {n : } [semiring R] {p : polynomial R} :
n p.support p.coeff n 0
theorem polynomial.not_mem_support_iff {R : Type u} {n : } [semiring R] {p : polynomial R} :
n p.support p.coeff n = 0
theorem polynomial.coeff_C {R : Type u} {a : R} {n : } [semiring R] :
(polynomial.C a).coeff n = ite (n = 0) a 0
@[simp]
theorem polynomial.coeff_C_zero {R : Type u} {a : R} [semiring R] :
theorem polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : } [semiring R] (h : n 0) :
theorem polynomial.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : polynomial R} (h : p q) :
@[simp]
theorem polynomial.C_inj {R : Type u} {a b : R} [semiring R] :
@[simp]
theorem polynomial.C_eq_zero {R : Type u} {a : R} [semiring R] :
theorem polynomial.ext_iff {R : Type u} [semiring R] {p q : polynomial R} :
p = q ∀ (n : ), p.coeff n = q.coeff n
@[ext]
theorem polynomial.ext {R : Type u} [semiring R] {p q : polynomial R} :
(∀ (n : ), p.coeff n = q.coeff n)p = q
theorem polynomial.add_hom_ext {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : polynomial R →+ M} (h : ∀ (n : ) (a : R), f ((polynomial.monomial n) a) = g ((polynomial.monomial n) a)) :
f = g
@[ext]
theorem polynomial.add_hom_ext' {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : polynomial R →+ M} (h : ∀ (n : ), f.comp (polynomial.monomial n).to_add_monoid_hom = g.comp (polynomial.monomial n).to_add_monoid_hom) :
f = g
@[ext]
theorem polynomial.lhom_ext' {R : Type u} [semiring R] {M : Type u_1} [add_comm_monoid M] [module R M] {f g : polynomial R →ₗ[R] M} (h : ∀ (n : ), f.comp (polynomial.monomial n) = g.comp (polynomial.monomial n)) :
f = g
theorem polynomial.eq_zero_of_eq_zero {R : Type u} [semiring R] (h : 0 = 1) (p : polynomial R) :
p = 0
theorem polynomial.support_monomial {R : Type u} [semiring R] (n : ) (a : R) (H : a 0) :
theorem polynomial.support_monomial' {R : Type u} [semiring R] (n : ) (a : R) :
theorem polynomial.monomial_eq_smul_X {R : Type u} {a : R} [semiring R] {n : } :
theorem polynomial.support_X_pow {R : Type u} [semiring R] (H : ¬1 = 0) (n : ) :
theorem polynomial.support_X_empty {R : Type u} [semiring R] (H : 1 = 0) :
theorem polynomial.support_X {R : Type u} [semiring R] (H : ¬1 = 0) :
theorem polynomial.monomial_left_inj {R : Type u_1} [semiring R] {a : R} (ha : a 0) {i j : } :
theorem polynomial.nat_cast_mul {R : Type u_1} [semiring R] (n : ) (p : polynomial R) :
(n) * p = n p
def polynomial.sum {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (f : R → S) :
S

Summing the values of a function applied to the coefficients of a polynomial

Equations
theorem polynomial.sum_def {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (f : R → S) :
p.sum f = ∑ (n : ) in p.support, f n (p.coeff n)
theorem polynomial.sum_eq_of_subset {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (f : R → S) (hf : ∀ (i : ), f i 0 = 0) (s : finset ) (hs : p.support s) :
p.sum f = ∑ (n : ) in s, f n (p.coeff n)
theorem polynomial.mul_eq_sum_sum {R : Type u} [semiring R] {p q : polynomial R} :
p * q = ∑ (i : ) in p.support, q.sum (λ (j : ) (a : R), (polynomial.monomial (i + j)) ((p.coeff i) * a))

Expressing the product of two polynomials as a double sum.

@[simp]
theorem polynomial.sum_zero_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (f : R → S) :
0.sum f = 0
@[simp]
theorem polynomial.sum_monomial_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (n : ) (a : R) (f : R → S) (hf : f n 0 = 0) :
((polynomial.monomial n) a).sum f = f n a
@[simp]
theorem polynomial.sum_C_index {R : Type u} [semiring R] {a : R} {β : Type u_1} [add_comm_monoid β] {f : R → β} (h : f 0 0 = 0) :
(polynomial.C a).sum f = f 0 a
@[simp]
theorem polynomial.sum_X_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] {f : R → S} (hf : f 1 0 = 0) :
theorem polynomial.sum_add_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p q : polynomial R) (f : R → S) (hf : ∀ (i : ), f i 0 = 0) (h_add : ∀ (a : ) (b₁ b₂ : R), f a (b₁ + b₂) = f a b₁ + f a b₂) :
(p + q).sum f = p.sum f + q.sum f
theorem polynomial.sum_add' {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (f g : R → S) :
p.sum (f + g) = p.sum f + p.sum g
theorem polynomial.sum_add {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (f g : R → S) :
p.sum (λ (n : ) (x : R), f n x + g n x) = p.sum f + p.sum g
theorem polynomial.sum_smul_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : polynomial R) (b : R) (f : R → S) (hf : ∀ (i : ), f i 0 = 0) :
(b p).sum f = p.sum (λ (n : ) (a : R), f n (b * a))
def polynomial.erase {R : Type u} [semiring R] (n : ) :

erase p n is the polynomial p in which the X^n term has been erased.

Equations
@[simp]
theorem polynomial.support_erase {R : Type u} [semiring R] (p : polynomial R) (n : ) :
theorem polynomial.monomial_add_erase {R : Type u} [semiring R] (p : polynomial R) (n : ) :
theorem polynomial.coeff_erase {R : Type u} [semiring R] (p : polynomial R) (n i : ) :
(polynomial.erase n p).coeff i = ite (i = n) 0 (p.coeff i)
@[simp]
theorem polynomial.erase_zero {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.erase_monomial {R : Type u} [semiring R] {n : } {a : R} :
@[simp]
theorem polynomial.erase_same {R : Type u} [semiring R] (p : polynomial R) (n : ) :
@[simp]
theorem polynomial.erase_ne {R : Type u} [semiring R] (p : polynomial R) (n i : ) (h : i n) :
@[instance]
def polynomial.ring {R : Type u} [ring R] :
Equations
@[simp]
theorem polynomial.coeff_neg {R : Type u} [ring R] (p : polynomial R) (n : ) :
(-p).coeff n = -p.coeff n
@[simp]
theorem polynomial.coeff_sub {R : Type u} [ring R] (p q : polynomial R) (n : ) :
(p - q).coeff n = p.coeff n - q.coeff n
@[simp]
theorem polynomial.monomial_neg {R : Type u} [ring R] (n : ) (a : R) :
@[simp]
theorem polynomial.support_neg {R : Type u} [ring R] {p : polynomial R} :
@[instance]
theorem polynomial.X_ne_zero {R : Type u} [semiring R] [nontrivial R] :
@[instance]
def polynomial.has_repr {R : Type u} [semiring R] [has_repr R] :
Equations