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 #

monomial n a is the polynomial a X^n. Note that monomial n is defined as an R-linear map.
C a is the constant polynomial a. Note that C is defined as a ring homomorphism.
X is the polynomial X, i.e., monomial 1 1.
p.sum f is ∑ n in p.support, f n (p.coeff n), i.e., one sums the values of functions applied to coefficients of the polynomial p.
p.erase n is the polynomial p in which one removes the c X^n term.

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,

sum_add_index states that (p + q).sum f = p.sum f + q.sum f;
sum_add states that p.sum (λ n x, f n x + g n x) = p.sum f + p.sum g.
Notation to refer to polynomial R, as R[X] or R[t].

Implementation #

Polynomials are defined using add_monoid_algebra R ℕ, where R is a semiring. The variable X commutes with every polynomial p: lemma X_mul proves the identity X * p =p * X. The relationship toadd_monoid_algebra R ℕis through a structure to make polynomials irreducible from the point of view of the kernel. Most operations are irreducible since Lean can not compute anyway withadd_monoid_algebra`. There are two exceptions that we make semireducible:

The zero polynomial, so that its coefficients are definitionally equal to 0.
The scalar action, to permit typeclass search to unfold it to resolve potential instance diamonds.

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

to_finsupp : add_monoid_algebra R ℕ

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 : R[X] → Prop) :

(∀ (p : R[X]), P p) ↔ ∀ (q : add_monoid_algebra R ℕ), P {to_finsupp := q}

theorem polynomial.exists_iff_exists_finsupp {R : Type u} [semiring R] (P : R[X] → Prop) :

(∃ (p : R[X]), P p) ↔ ∃ (q : add_monoid_algebra R ℕ), P {to_finsupp := q}

Conversions to and from `add_monoid_algebra` #

Since polynomial R is not defeq to add_monoid_algebra R ℕ, but instead is a structure wrapping it, we have to copy across all the arithmetic operators manually, along with the lemmas about how they unfold around polynomial.of_finsupp and polynomial.to_finsupp.

noncomputable def polynomial.monomial_fun {R : Type u} [semiring R] (n : ℕ) (a : R) :

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

Equations

polynomial.monomial_fun n a = {to_finsupp := finsupp.single n a}

@[protected, instance]

noncomputable def polynomial.has_zero {R : Type u} [semiring R] :

Equations

polynomial.has_zero = {zero := {to_finsupp := 0}}

@[protected, instance]

noncomputable def polynomial.has_one {R : Type u} [semiring R] :

Equations

polynomial.has_one = {one := polynomial.monomial_fun 0 1}

@[protected, instance]

noncomputable def polynomial.has_add {R : Type u} [semiring R] :

Equations

polynomial.has_add = {add := add _inst_1}

@[protected, instance]

noncomputable def polynomial.has_neg {R : Type u} [ring R] :

Equations

polynomial.has_neg = {neg := neg _inst_2}

@[protected, instance]

noncomputable def polynomial.has_sub {R : Type u} [ring R] :

Equations

polynomial.has_sub = {sub := λ (a b : R[X]), a + -b}

@[protected, instance]

noncomputable def polynomial.has_mul {R : Type u} [semiring R] :

Equations

polynomial.has_mul = {mul := mul _inst_1}

@[protected, instance]

noncomputable def polynomial.has_scalar {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] :

has_scalar S R[X]

Equations

polynomial.has_scalar = {smul := λ (r : S) (p : R[X]), {to_finsupp := r • p.to_finsupp}}

@[protected, instance]

noncomputable def polynomial.has_pow {R : Type u} [semiring R] :

has_pow R[X] ℕ

Equations

polynomial.has_pow = {pow := λ (p : R[X]) (n : ℕ), npow_rec n p}

@[simp]

theorem polynomial.of_finsupp_zero {R : Type u} [semiring R] :

{to_finsupp := 0} = 0

@[simp]

theorem polynomial.of_finsupp_one {R : Type u} [semiring R] :

{to_finsupp := 1} = 1

@[simp]

theorem polynomial.of_finsupp_add {R : Type u} [semiring R] {a b : add_monoid_algebra R ℕ} :

{to_finsupp := a + b} = {to_finsupp := a} + {to_finsupp := b}

@[simp]

theorem polynomial.of_finsupp_neg {R : Type u} [ring R] {a : add_monoid_algebra R ℕ} :

{to_finsupp := -a} = -{to_finsupp := a}

@[simp]

theorem polynomial.of_finsupp_sub {R : Type u} [ring R] {a b : add_monoid_algebra R ℕ} :

{to_finsupp := a - b} = {to_finsupp := a} - {to_finsupp := b}

@[simp]

theorem polynomial.of_finsupp_mul {R : Type u} [semiring R] (a b : add_monoid_algebra R ℕ) :

{to_finsupp := a * b} = {to_finsupp := a} * {to_finsupp := b}

@[simp]

theorem polynomial.of_finsupp_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] (a : S) (b : add_monoid_algebra R ℕ) :

{to_finsupp := a • b} = a • {to_finsupp := b}

@[simp]

theorem polynomial.of_finsupp_pow {R : Type u} [semiring R] (a : add_monoid_algebra R ℕ) (n : ℕ) :

{to_finsupp := a ^ n} = {to_finsupp := a} ^ n

@[simp]

theorem polynomial.to_finsupp_zero {R : Type u} [semiring R] :

0.to_finsupp = 0

@[simp]

theorem polynomial.to_finsupp_one {R : Type u} [semiring R] :

1.to_finsupp = 1

@[simp]

theorem polynomial.to_finsupp_add {R : Type u} [semiring R] (a b : R[X]) :

(a + b).to_finsupp = a.to_finsupp + b.to_finsupp

@[simp]

theorem polynomial.to_finsupp_neg {R : Type u} [ring R] (a : R[X]) :

(-a).to_finsupp = -a.to_finsupp

@[simp]

theorem polynomial.to_finsupp_sub {R : Type u} [ring R] (a b : R[X]) :

(a - b).to_finsupp = a.to_finsupp - b.to_finsupp

@[simp]

theorem polynomial.to_finsupp_mul {R : Type u} [semiring R] (a b : R[X]) :

(a * b).to_finsupp = (a.to_finsupp) * b.to_finsupp

@[simp]

theorem polynomial.to_finsupp_smul {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] (a : S) (b : R[X]) :

(a • b).to_finsupp = a • b.to_finsupp

@[simp]

theorem polynomial.to_finsupp_pow {R : Type u} [semiring R] (a : R[X]) (n : ℕ) :

(a ^ n).to_finsupp = a.to_finsupp ^ n

theorem is_smul_regular.polynomial {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] {a : S} (ha : is_smul_regular R a) :

is_smul_regular R[X] a

theorem polynomial.to_finsupp_injective {R : Type u} [semiring R] :

function.injective polynomial.to_finsupp

@[simp]

theorem polynomial.to_finsupp_inj {R : Type u} [semiring R] {a b : R[X]} :

a.to_finsupp = b.to_finsupp ↔ a = b

@[simp]

theorem polynomial.to_finsupp_eq_zero {R : Type u} [semiring R] {a : R[X]} :

a.to_finsupp = 0 ↔ a = 0

@[simp]

theorem polynomial.to_finsupp_eq_one {R : Type u} [semiring R] {a : R[X]} :

a.to_finsupp = 1 ↔ a = 1

theorem polynomial.of_finsupp_inj {R : Type u} [semiring R] {a b : add_monoid_algebra R ℕ} :

{to_finsupp := a} = {to_finsupp := b} ↔ a = b

A more convenient spelling of polynomial.of_finsupp.inj_eq in terms of iff.

@[simp]

theorem polynomial.of_finsupp_eq_zero {R : Type u} [semiring R] {a : add_monoid_algebra R ℕ} :

{to_finsupp := a} = 0 ↔ a = 0

@[simp]

theorem polynomial.of_finsupp_eq_one {R : Type u} [semiring R] {a : add_monoid_algebra R ℕ} :

{to_finsupp := a} = 1 ↔ a = 1

@[protected, instance]

noncomputable def polynomial.inhabited {R : Type u} [semiring R] :

Equations

polynomial.inhabited = {default := 0}

@[protected, instance]

noncomputable def polynomial.semiring {R : Type u} [semiring R] :

Equations

polynomial.semiring = function.injective.semiring polynomial.to_finsupp polynomial.to_finsupp_injective polynomial.to_finsupp_zero polynomial.to_finsupp_one polynomial.to_finsupp_add polynomial.to_finsupp_mul polynomial.semiring._proof_1 polynomial.to_finsupp_pow

@[protected, instance]

noncomputable def polynomial.distrib_mul_action {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] :

distrib_mul_action S R[X]

Equations

polynomial.distrib_mul_action = function.injective.distrib_mul_action {to_fun := polynomial.to_finsupp _inst_1, map_zero' := _, map_add' := _} polynomial.to_finsupp_injective polynomial.to_finsupp_smul

@[protected, instance]

def polynomial.has_faithful_scalar {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [has_faithful_scalar S R] :

has_faithful_scalar S R[X]

@[protected, instance]

noncomputable def polynomial.module {R : Type u} [semiring R] {S : Type u_1} [semiring S] [module S R] :

Equations

polynomial.module = function.injective.module S {to_fun := polynomial.to_finsupp _inst_1, map_zero' := _, map_add' := _} polynomial.to_finsupp_injective polynomial.module._proof_1

@[protected, 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] :

smul_comm_class S₁ S₂ R[X]

@[protected, 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] :

is_scalar_tower S₁ S₂ R[X]

@[protected, instance]

def polynomial.is_central_scalar {R : Type u} [semiring R] {S : Type u_1} [monoid S] [distrib_mul_action S R] [distrib_mul_action Sᵐᵒᵖ R] [is_central_scalar S R] :

is_central_scalar S R[X]

@[protected, instance]

noncomputable def polynomial.unique {R : Type u} [semiring R] [subsingleton R] :

Equations

polynomial.unique = {to_inhabited := {default := default polynomial.inhabited}, uniq := _}

@[simp]

theorem polynomial.to_finsupp_iso_symm_apply (R : Type u) [semiring R] (to_finsupp : add_monoid_algebra R ℕ) :

⇑((polynomial.to_finsupp_iso R).symm) to_finsupp = {to_finsupp := to_finsupp}

def polynomial.to_finsupp_iso (R : Type u) [semiring R] :

R[X] ≃+* add_monoid_algebra R ℕ

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

Equations

polynomial.to_finsupp_iso R = {to_fun := polynomial.to_finsupp _inst_1, inv_fun := polynomial.of_finsupp _inst_1, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

@[simp]

theorem polynomial.to_finsupp_iso_apply (R : Type u) [semiring R] (self : R[X]) :

⇑(polynomial.to_finsupp_iso R) self = self.to_finsupp

theorem polynomial.of_finsupp_sum {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → add_monoid_algebra R ℕ) :

{to_finsupp := ∑ (i : ι) in s, f i} = ∑ (i : ι) in s, {to_finsupp := f i}

theorem polynomial.to_finsupp_sum {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι → R[X]) :

(∑ (i : ι) in s, f i).to_finsupp = ∑ (i : ι) in s, (f i).to_finsupp

@[simp]

def polynomial.support {R : Type u} [semiring R] :

R[X] → finset ℕ

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

Equations

{to_finsupp := p}.support = p.support

@[simp]

theorem polynomial.support_of_finsupp {R : Type u} [semiring R] (p : add_monoid_algebra R ℕ) :

{to_finsupp := p}.support = p.support

@[simp]

theorem polynomial.support_zero {R : Type u} [semiring R] :

0.support = ∅

@[simp]

theorem polynomial.support_eq_empty {R : Type u} [semiring R] {p : R[X]} :

p.support = ∅ ↔ p = 0

theorem polynomial.card_support_eq_zero {R : Type u} [semiring R] {p : R[X]} :

p.support.card = 0 ↔ p = 0

noncomputable def polynomial.monomial {R : Type u} [semiring R] (n : ℕ) :

R →ₗ[R] R[X]

monomial s a is the monomial a * X^s

Equations

polynomial.monomial n = {to_fun := polynomial.monomial_fun n, map_add' := _, map_smul' := _}

@[simp]

theorem polynomial.to_finsupp_monomial {R : Type u} [semiring R] (n : ℕ) (r : R) :

(⇑(polynomial.monomial n) r).to_finsupp = finsupp.single n r

@[simp]

theorem polynomial.of_finsupp_single {R : Type u} [semiring R] (n : ℕ) (r : R) :

{to_finsupp := finsupp.single n r} = ⇑(polynomial.monomial n) r

@[simp]

theorem polynomial.monomial_zero_right {R : Type u} [semiring R] (n : ℕ) :

⇑(polynomial.monomial n) 0 = 0

theorem polynomial.monomial_zero_one {R : Type u} [semiring R] :

⇑(polynomial.monomial 0) 1 = 1

theorem polynomial.monomial_add {R : Type u} [semiring R] (n : ℕ) (r s : R) :

⇑(polynomial.monomial n) (r + s) = ⇑(polynomial.monomial n) r + ⇑(polynomial.monomial n) s

theorem polynomial.monomial_mul_monomial {R : Type u} [semiring R] (n m : ℕ) (r s : R) :

(⇑(polynomial.monomial n) r) * ⇑(polynomial.monomial m) s = ⇑(polynomial.monomial (n + m)) (r * s)

@[simp]

theorem polynomial.monomial_pow {R : Type u} [semiring R] (n : ℕ) (r : R) (k : ℕ) :

⇑(polynomial.monomial n) r ^ k = ⇑(polynomial.monomial (n * k)) (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) :

a • ⇑(polynomial.monomial n) b = ⇑(polynomial.monomial n) (a • b)

theorem polynomial.monomial_injective {R : Type u} [semiring R] (n : ℕ) :

function.injective ⇑(polynomial.monomial n)

@[simp]

theorem polynomial.monomial_eq_zero_iff {R : Type u} [semiring R] (t : R) (n : ℕ) :

⇑(polynomial.monomial n) t = 0 ↔ t = 0

theorem polynomial.support_add {R : Type u} [semiring R] {p q : R[X]} :

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

noncomputable def polynomial.C {R : Type u} [semiring R] :

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

Equations

polynomial.C = {to_fun := (polynomial.monomial 0).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem polynomial.monomial_zero_left {R : Type u} [semiring R] (a : R) :

⇑(polynomial.monomial 0) a = ⇑polynomial.C a

@[simp]

theorem polynomial.to_finsupp_C {R : Type u} [semiring R] (a : R) :

(⇑polynomial.C a).to_finsupp = finsupp.single 0 a

theorem polynomial.C_0 {R : Type u} [semiring R] :

⇑polynomial.C 0 = 0

theorem polynomial.C_1 {R : Type u} [semiring R] :

⇑polynomial.C 1 = 1

theorem polynomial.C_mul {R : Type u} {a b : R} [semiring R] :

⇑polynomial.C (a * b) = (⇑polynomial.C a) * ⇑polynomial.C b

theorem polynomial.C_add {R : Type u} {a b : R} [semiring R] :

⇑polynomial.C (a + b) = ⇑polynomial.C a + ⇑polynomial.C b

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

s • ⇑polynomial.C r = ⇑polynomial.C (s • r)

@[simp]

theorem polynomial.C_bit0 {R : Type u} {a : R} [semiring R] :

⇑polynomial.C (bit0 a) = bit0 (⇑polynomial.C a)

@[simp]

theorem polynomial.C_bit1 {R : Type u} {a : R} [semiring R] :

⇑polynomial.C (bit1 a) = bit1 (⇑polynomial.C a)

theorem polynomial.C_pow {R : Type u} {a : R} {n : ℕ} [semiring R] :

⇑polynomial.C (a ^ n) = ⇑polynomial.C a ^ n

@[simp]

theorem polynomial.C_eq_nat_cast {R : Type u} [semiring R] (n : ℕ) :

⇑polynomial.C ↑n = ↑n

@[simp]

theorem polynomial.C_mul_monomial {R : Type u} {a b : R} {n : ℕ} [semiring R] :

(⇑polynomial.C a) * ⇑(polynomial.monomial n) b = ⇑(polynomial.monomial n) (a * b)

@[simp]

theorem polynomial.monomial_mul_C {R : Type u} {a b : R} {n : ℕ} [semiring R] :

(⇑(polynomial.monomial n) a) * ⇑polynomial.C b = ⇑(polynomial.monomial n) (a * b)

noncomputable def polynomial.X {R : Type u} [semiring R] :

X is the polynomial variable (aka indeterminate).

Equations

polynomial.X = ⇑(polynomial.monomial 1) 1

theorem polynomial.monomial_one_one_eq_X {R : Type u} [semiring R] :

⇑(polynomial.monomial 1) 1 = polynomial.X

theorem polynomial.monomial_one_right_eq_X_pow {R : Type u} [semiring R] (n : ℕ) :

⇑(polynomial.monomial n) 1 = polynomial.X ^ n

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

polynomial.X * p = p * polynomial.X

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

theorem polynomial.X_pow_mul {R : Type u} [semiring R] {p : R[X]} {n : ℕ} :

(polynomial.X ^ n) * p = p * polynomial.X ^ n

@[simp]

theorem polynomial.X_mul_C {R : Type u} [semiring R] (r : R) :

polynomial.X * ⇑polynomial.C r = (⇑polynomial.C r) * polynomial.X

Prefer putting constants to the left of X.

This lemma is the loop-avoiding simp version of polynomial.X_mul.

@[simp]

theorem polynomial.X_pow_mul_C {R : Type u} [semiring R] (r : R) (n : ℕ) :

(polynomial.X ^ n) * ⇑polynomial.C r = (⇑polynomial.C r) * polynomial.X ^ n

Prefer putting constants to the left of X ^ n.

This lemma is the loop-avoiding simp version of X_pow_mul.

theorem polynomial.X_pow_mul_assoc {R : Type u} [semiring R] {p q : R[X]} {n : ℕ} :

(p * polynomial.X ^ n) * q = (p * q) * polynomial.X ^ n

@[simp]

theorem polynomial.X_pow_mul_assoc_C {R : Type u} [semiring R] {p : R[X]} {n : ℕ} (r : R) :

(p * polynomial.X ^ n) * ⇑polynomial.C r = (p * ⇑polynomial.C r) * polynomial.X ^ n

Prefer putting constants to the left of X ^ n.

This lemma is the loop-avoiding simp version of X_pow_mul_assoc.

theorem polynomial.commute_X {R : Type u} [semiring R] (p : R[X]) :

commute polynomial.X p

theorem polynomial.commute_X_pow {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

commute (polynomial.X ^ n) p

@[simp]

theorem polynomial.monomial_mul_X {R : Type u} [semiring R] (n : ℕ) (r : R) :

(⇑(polynomial.monomial n) r) * polynomial.X = ⇑(polynomial.monomial (n + 1)) r

@[simp]

theorem polynomial.monomial_mul_X_pow {R : Type u} [semiring R] (n : ℕ) (r : R) (k : ℕ) :

(⇑(polynomial.monomial n) r) * polynomial.X ^ k = ⇑(polynomial.monomial (n + k)) r

@[simp]

theorem polynomial.X_mul_monomial {R : Type u} [semiring R] (n : ℕ) (r : R) :

polynomial.X * ⇑(polynomial.monomial n) r = ⇑(polynomial.monomial (n + 1)) r

@[simp]

theorem polynomial.X_pow_mul_monomial {R : Type u} [semiring R] (k n : ℕ) (r : R) :

(polynomial.X ^ k) * ⇑(polynomial.monomial n) r = ⇑(polynomial.monomial (n + k)) r

@[simp]

def polynomial.coeff {R : Type u} [semiring R] :

R[X] → ℕ → R

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

Equations

{to_finsupp := p}.coeff = ⇑p

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

polynomial.X.coeff 1 = 1

@[simp]

theorem polynomial.coeff_X_zero {R : Type u} [semiring R] :

polynomial.X.coeff 0 = 0

@[simp]

theorem polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : ℕ} [semiring R] :

(⇑(polynomial.monomial (n + 1)) a).coeff 0 = 0

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

polynomial.X.coeff n = 0

@[simp]

theorem polynomial.mem_support_iff {R : Type u} {n : ℕ} [semiring R] {p : R[X]} :

n ∈ p.support ↔ p.coeff n ≠ 0

theorem polynomial.not_mem_support_iff {R : Type u} {n : ℕ} [semiring R] {p : R[X]} :

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

(⇑polynomial.C a).coeff 0 = a

theorem polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) :

(⇑polynomial.C a).coeff n = 0

theorem polynomial.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : R[X]} (h : p ≠ q) :

theorem polynomial.monomial_eq_C_mul_X {R : Type u} {a : R} [semiring R] {n : ℕ} :

⇑(polynomial.monomial n) a = (⇑polynomial.C a) * polynomial.X ^ n

@[simp]

theorem polynomial.C_inj {R : Type u} {a b : R} [semiring R] :

⇑polynomial.C a = ⇑polynomial.C b ↔ a = b

@[simp]

theorem polynomial.C_eq_zero {R : Type u} {a : R} [semiring R] :

⇑polynomial.C a = 0 ↔ a = 0

theorem polynomial.ext_iff {R : Type u} [semiring R] {p q : R[X]} :

p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

@[ext]

theorem polynomial.ext {R : Type u} [semiring R] {p q : R[X]} :

(∀ (n : ℕ), p.coeff n = q.coeff n) → p = q

theorem polynomial.add_submonoid_closure_set_of_eq_monomial {R : Type u} [semiring R] :

add_submonoid.closure {p : R[X] | ∃ (n : ℕ) (a : R), p = ⇑(polynomial.monomial n) a} = ⊤

Monomials generate the additive monoid of polynomials.

theorem polynomial.add_hom_ext {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : R[X] →+ 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 : R[X] →+ 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 : R[X] →ₗ[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 : R[X]) :

p = 0

theorem polynomial.support_monomial {R : Type u} [semiring R] (n : ℕ) (a : R) (H : a ≠ 0) :

(⇑(polynomial.monomial n) a).support = {n}

theorem polynomial.support_monomial' {R : Type u} [semiring R] (n : ℕ) (a : R) :

(⇑(polynomial.monomial n) a).support ⊆ {n}

theorem polynomial.X_pow_eq_monomial {R : Type u} [semiring R] (n : ℕ) :

polynomial.X ^ n = ⇑(polynomial.monomial n) 1

theorem polynomial.monomial_eq_smul_X {R : Type u} {a : R} [semiring R] {n : ℕ} :

⇑(polynomial.monomial n) a = a • polynomial.X ^ n

theorem polynomial.support_X_pow {R : Type u} [semiring R] (H : ¬1 = 0) (n : ℕ) :

(polynomial.X ^ n).support = {n}

theorem polynomial.support_X_empty {R : Type u} [semiring R] (H : 1 = 0) :

polynomial.X.support = ∅

theorem polynomial.support_X {R : Type u} [semiring R] (H : ¬1 = 0) :

polynomial.X.support = {1}

theorem polynomial.monomial_left_inj {R : Type u_1} [semiring R] {a : R} (ha : a ≠ 0) {i j : ℕ} :

⇑(polynomial.monomial i) a = ⇑(polynomial.monomial j) a ↔ i = j

theorem polynomial.nat_cast_mul {R : Type u_1} [semiring R] (n : ℕ) (p : R[X]) :

(↑n) * p = n • p

def polynomial.sum {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : R[X]) (f : ℕ → R → S) :

S

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

Equations

p.sum f = ∑ (n : ℕ) in p.support, f n (p.coeff n)

theorem polynomial.sum_def {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p : R[X]) (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 : R[X]) (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 : R[X]} :

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

polynomial.X.sum f = f 1 1

theorem polynomial.sum_add_index {R : Type u} [semiring R] {S : Type u_1} [add_comm_monoid S] (p q : R[X]) (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 : R[X]) (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 : R[X]) (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 : R[X]) (b : R) (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) :

(b • p).sum f = p.sum (λ (n : ℕ) (a : R), f n (b * a))

noncomputable def polynomial.erase {R : Type u} [semiring R] (n : ℕ) :

R[X] → R[X]

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

Equations

polynomial.erase n {to_finsupp := p} = {to_finsupp := finsupp.erase n p}

@[simp]

theorem polynomial.to_finsupp_erase {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

(polynomial.erase n p).to_finsupp = finsupp.erase n p.to_finsupp

@[simp]

theorem polynomial.of_finsupp_erase {R : Type u} [semiring R] (p : add_monoid_algebra R ℕ) (n : ℕ) :

{to_finsupp := finsupp.erase n p} = polynomial.erase n {to_finsupp := p}

@[simp]

theorem polynomial.support_erase {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

(polynomial.erase n p).support = p.support.erase n

theorem polynomial.monomial_add_erase {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

⇑(polynomial.monomial n) (p.coeff n) + polynomial.erase n p = p

theorem polynomial.coeff_erase {R : Type u} [semiring R] (p : R[X]) (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 : ℕ) :

polynomial.erase n 0 = 0

@[simp]

theorem polynomial.erase_monomial {R : Type u} [semiring R] {n : ℕ} {a : R} :

polynomial.erase n (⇑(polynomial.monomial n) a) = 0

@[simp]

theorem polynomial.erase_same {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

(polynomial.erase n p).coeff n = 0

@[simp]

theorem polynomial.erase_ne {R : Type u} [semiring R] (p : R[X]) (n i : ℕ) (h : i ≠ n) :

(polynomial.erase n p).coeff i = p.coeff i

noncomputable def polynomial.update {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (a : R) :

Replace the coefficient of a p : polynomial p at a given degree n : ℕ by a given value a : R. If a = 0, this is equal to p.erase n If p.nat_degree < n and a ≠ 0, this increases the degree to n.

Equations

p.update n a = {to_finsupp := finsupp.update p.to_finsupp n a}

theorem polynomial.coeff_update {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (a : R) :

(p.update n a).coeff = function.update p.coeff n a

theorem polynomial.coeff_update_apply {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (a : R) (i : ℕ) :

(p.update n a).coeff i = ite (i = n) a (p.coeff i)

@[simp]

theorem polynomial.coeff_update_same {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (a : R) :

(p.update n a).coeff n = a

theorem polynomial.coeff_update_ne {R : Type u} [semiring R] (p : R[X]) {n : ℕ} (a : R) {i : ℕ} (h : i ≠ n) :

(p.update n a).coeff i = p.coeff i

@[simp]

theorem polynomial.update_zero_eq_erase {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

p.update n 0 = polynomial.erase n p

theorem polynomial.support_update {R : Type u} [semiring R] (p : R[X]) (n : ℕ) (a : R) [decidable (a = 0)] :

(p.update n a).support = ite (a = 0) (p.support.erase n) (insert n p.support)

theorem polynomial.support_update_zero {R : Type u} [semiring R] (p : R[X]) (n : ℕ) :

(p.update n 0).support = p.support.erase n

theorem polynomial.support_update_ne_zero {R : Type u} [semiring R] (p : R[X]) (n : ℕ) {a : R} (ha : a ≠ 0) :

(p.update n a).support = insert n p.support

@[protected, instance]

noncomputable def polynomial.comm_semiring {R : Type u} [comm_semiring R] :

comm_semiring R[X]

Equations

polynomial.comm_semiring = function.injective.comm_semiring polynomial.to_finsupp polynomial.comm_semiring._proof_1 polynomial.comm_semiring._proof_2 polynomial.comm_semiring._proof_3 polynomial.comm_semiring._proof_4 polynomial.comm_semiring._proof_5 polynomial.comm_semiring._proof_6 polynomial.comm_semiring._proof_7

@[protected, instance]

noncomputable def polynomial.ring {R : Type u} [ring R] :

Equations

polynomial.ring = function.injective.ring polynomial.to_finsupp polynomial.ring._proof_1 polynomial.ring._proof_2 polynomial.ring._proof_3 polynomial.ring._proof_4 polynomial.ring._proof_5 polynomial.to_finsupp_neg polynomial.to_finsupp_sub polynomial.ring._proof_6 polynomial.ring._proof_7 polynomial.ring._proof_8

@[simp]

theorem polynomial.coeff_neg {R : Type u} [ring R] (p : R[X]) (n : ℕ) :

(-p).coeff n = -p.coeff n

@[simp]

theorem polynomial.coeff_sub {R : Type u} [ring R] (p q : R[X]) (n : ℕ) :

(p - q).coeff n = p.coeff n - q.coeff n

@[simp]

theorem polynomial.monomial_neg {R : Type u} [ring R] (n : ℕ) (a : R) :

⇑(polynomial.monomial n) (-a) = -⇑(polynomial.monomial n) a

@[simp]

theorem polynomial.support_neg {R : Type u} [ring R] {p : R[X]} :

(-p).support = p.support

@[simp]

theorem polynomial.C_eq_int_cast {R : Type u} [ring R] (n : ℤ) :

⇑polynomial.C ↑n = ↑n

@[protected, instance]

noncomputable def polynomial.comm_ring {R : Type u} [comm_ring R] :

Equations

polynomial.comm_ring = function.injective.comm_ring polynomial.to_finsupp polynomial.comm_ring._proof_1 polynomial.comm_ring._proof_2 polynomial.comm_ring._proof_3 polynomial.comm_ring._proof_4 polynomial.comm_ring._proof_5 polynomial.comm_ring._proof_6 polynomial.comm_ring._proof_7 polynomial.comm_ring._proof_8 polynomial.comm_ring._proof_9 polynomial.comm_ring._proof_10

@[protected, instance]

def polynomial.nontrivial {R : Type u} [semiring R] [nontrivial R] :

nontrivial R[X]

theorem polynomial.X_ne_zero {R : Type u} [semiring R] [nontrivial R] :

polynomial.X ≠ 0

@[simp]

theorem polynomial.nontrivial_iff {R : Type u} [semiring R] :

nontrivial R[X] ↔ nontrivial R

@[protected, instance]

noncomputable def polynomial.has_repr {R : Type u} [semiring R] [has_repr R] :

Equations

polynomial.has_repr = {repr := λ (p : R[X]), ite (p = 0) "0" (list.foldr (λ (n : ℕ) (a : string), a ++ ite (a = "") "" " + " ++ ite (n = 0) ("C (" ++ repr (p.coeff n) ++ ")") (ite (n = 1) (ite (p.coeff n = 1) "X" ("C (" ++ repr (p.coeff n) ++ ") * X")) (ite (p.coeff n = 1) ("X ^ " ++ repr n) ("C (" ++ repr (p.coeff n) ++ ") * X ^ " ++ repr n)))) "" (finset.sort has_le.le p.support))}