# mathlib3documentation

data.polynomial.basic

# Theory of univariate polynomials #

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

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 to `add_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 with `add_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 `R[X]` 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 :

`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`.

Instances for `polynomial`
theorem polynomial.forall_iff_forall_finsupp {R : Type u} [semiring R] (P : Prop) :
( (p : , P p) (q : , P {to_finsupp := q}
theorem polynomial.exists_iff_exists_finsupp {R : Type u} [semiring R] (P : Prop) :
( (p : , P p) (q : , P {to_finsupp := q}
@[simp]
theorem polynomial.eta {R : Type u} [semiring R] (f : polynomial R) :

### Conversions to and from `add_monoid_algebra`#

Since `R[X]` 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`.

@[protected, instance]
noncomputable def polynomial.has_zero {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_one {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_add {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_neg {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_sub {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_mul {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.smul_zero_class {R : Type u} [semiring R] {S : Type u_1} [ R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_pow {R : Type u} [semiring R] :
Equations
@[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 : } :
{to_finsupp := a + b} = {to_finsupp := a} + {to_finsupp := b}
@[simp]
theorem polynomial.of_finsupp_neg {R : Type u} [ring R] {a : } :
{to_finsupp := -a} = -{to_finsupp := a}
@[simp]
theorem polynomial.of_finsupp_sub {R : Type u} [ring R] {a b : } :
{to_finsupp := a - b} = {to_finsupp := a} - {to_finsupp := b}
@[simp]
theorem polynomial.of_finsupp_mul {R : Type u} [semiring R] (a b : ) :
{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} [ R] (a : S) (b : ) :
{to_finsupp := a b} = a {to_finsupp := b}
@[simp]
theorem polynomial.of_finsupp_pow {R : Type u} [semiring R] (a : ) (n : ) :
{to_finsupp := a ^ n} = {to_finsupp := a} ^ n
@[simp]
theorem polynomial.to_finsupp_zero {R : Type u} [semiring R] :
@[simp]
theorem polynomial.to_finsupp_one {R : Type u} [semiring R] :
@[simp]
theorem polynomial.to_finsupp_add {R : Type u} [semiring R] (a b : polynomial R) :
(a + b).to_finsupp =
@[simp]
theorem polynomial.to_finsupp_neg {R : Type u} [ring R] (a : polynomial R) :
@[simp]
theorem polynomial.to_finsupp_sub {R : Type u} [ring R] (a b : polynomial R) :
(a - b).to_finsupp =
@[simp]
theorem polynomial.to_finsupp_mul {R : Type u} [semiring R] (a b : polynomial R) :
(a * b).to_finsupp =
@[simp]
theorem polynomial.to_finsupp_smul {R : Type u} [semiring R] {S : Type u_1} [ R] (a : S) (b : polynomial R) :
@[simp]
theorem polynomial.to_finsupp_pow {R : Type u} [semiring R] (a : polynomial R) (n : ) :
theorem is_smul_regular.polynomial {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] {a : S} (ha : a) :
@[simp]
theorem polynomial.to_finsupp_inj {R : Type u} [semiring R] {a b : polynomial R} :
a = b
@[simp]
theorem polynomial.to_finsupp_eq_zero {R : Type u} [semiring R] {a : polynomial R} :
a.to_finsupp = 0 a = 0
@[simp]
theorem polynomial.to_finsupp_eq_one {R : Type u} [semiring R] {a : polynomial R} :
a.to_finsupp = 1 a = 1
theorem polynomial.of_finsupp_inj {R : Type u} [semiring R] {a b : } :
{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 : } :
{to_finsupp := a} = 0 a = 0
@[simp]
theorem polynomial.of_finsupp_eq_one {R : Type u} [semiring R] {a : } :
{to_finsupp := a} = 1 a = 1
@[protected, instance]
noncomputable def polynomial.inhabited {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.has_nat_cast {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.semiring {R : Type u} [semiring R] :
Equations
@[protected, instance]
noncomputable def polynomial.distrib_smul {R : Type u} [semiring R] {S : Type u_1} [ R] :
Equations
@[protected, instance]
noncomputable def polynomial.distrib_mul_action {R : Type u} [semiring R] {S : Type u_1} [monoid S] [ R] :
Equations
@[protected, instance]
def polynomial.has_faithful_smul {R : Type u} [semiring R] {S : Type u_1} [ R] [ R] :
@[protected, instance]
noncomputable def polynomial.module {R : Type u} [semiring R] {S : Type u_1} [semiring S] [ R] :
Equations
@[protected, instance]
def polynomial.smul_comm_class {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [ R] [ R] [ S₂ R] :
S₂ (polynomial R)
@[protected, instance]
def polynomial.is_scalar_tower {R : Type u} [semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [has_smul S₁ S₂] [ R] [ R] [ S₂ R] :
S₂ (polynomial R)
@[protected, instance]
def polynomial.is_scalar_tower_right {α : Type u_1} {K : Type u_2} [semiring K] [ K] [ K] :
@[protected, instance]
def polynomial.is_central_scalar {R : Type u} [semiring R] {S : Type u_1} [ R] [ R] [ R] :
@[protected, instance]
noncomputable def polynomial.unique {R : Type u} [semiring R] [subsingleton R] :
Equations
@[simp]
theorem polynomial.to_finsupp_iso_symm_apply (R : Type u) [semiring R] (to_finsupp : ) :
to_finsupp = {to_finsupp := to_finsupp}

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
@[simp]
theorem polynomial.to_finsupp_iso_apply (R : Type u) [semiring R] (self : polynomial R) :
self = self.to_finsupp
theorem polynomial.of_finsupp_sum {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι ) :
{to_finsupp := s.sum (λ (i : ι), f i)} = s.sum (λ (i : ι), {to_finsupp := f i})
theorem polynomial.to_finsupp_sum {R : Type u} [semiring R] {ι : Type u_1} (s : finset ι) (f : ι ) :
(s.sum (λ (i : ι), f i)).to_finsupp = s.sum (λ (i : ι), (f i).to_finsupp)
@[simp]
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_of_finsupp {R : Type u} [semiring R] (p : ) :
@[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 = 0
theorem polynomial.card_support_eq_zero {R : Type u} [semiring R] {p : polynomial R} :
p.support.card = 0 p = 0
noncomputable def polynomial.monomial {R : Type u} [semiring R] (n : ) :

`monomial s a` is the monomial `a * X^s`

Equations
@[simp]
theorem polynomial.to_finsupp_monomial {R : Type u} [semiring R] (n : ) (r : R) :
@[simp]
theorem polynomial.of_finsupp_single {R : Type u} [semiring R] (n : ) (r : R) :
{to_finsupp := r} = r
@[simp]
theorem polynomial.monomial_zero_right {R : Type u} [semiring R] (n : ) :
0 = 0
theorem polynomial.monomial_zero_one {R : Type u} [semiring R] :
1 = 1
theorem polynomial.monomial_add {R : Type u} [semiring R] (n : ) (r s : R) :
(r + s) = r + s
theorem polynomial.monomial_mul_monomial {R : Type u} [semiring R] (n m : ) (r s : R) :
r * s = (polynomial.monomial (n + m)) (r * s)
@[simp]
theorem polynomial.monomial_pow {R : Type u} [semiring R] (n : ) (r : R) (k : ) :
r ^ k = (polynomial.monomial (n * k)) (r ^ k)
theorem polynomial.smul_monomial {R : Type u} [semiring R] {S : Type u_1} [ R] (a : S) (n : ) (b : R) :
a b = (a b)
theorem polynomial.monomial_injective {R : Type u} [semiring R] (n : ) :
@[simp]
theorem polynomial.monomial_eq_zero_iff {R : Type u} [semiring R] (t : R) (n : ) :
t = 0 t = 0
theorem polynomial.support_add {R : Type u} [semiring R] {p q : polynomial R} :
noncomputable 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) :
@[simp]
theorem polynomial.to_finsupp_C {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} [ 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] :
= (a * b)
@[simp]
theorem polynomial.monomial_mul_C {R : Type u} {a b : R} {n : } [semiring R] :
= (a * b)
noncomputable def polynomial.X {R : Type u} [semiring R] :

`X` is the polynomial variable (aka indeterminate).

Equations
@[simp]
theorem polynomial.to_finsupp_X {R : Type u} [semiring R] :
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 : } :
* p = p *
@[simp]
theorem polynomial.X_mul_C {R : Type u} [semiring R] (r : R) :

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

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 : polynomial R} {n : } :
p * * q = p * q *
@[simp]
theorem polynomial.X_pow_mul_assoc_C {R : Type u} [semiring R] {p : polynomial R} {n : } (r : R) :
p * * = *

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 : polynomial R) :
theorem polynomial.commute_X_pow {R : Type u} [semiring R] (p : polynomial R) (n : ) :
@[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) :
@[simp]
def polynomial.coeff {R : Type u} [semiring R] :

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

Equations
@[simp]
theorem polynomial.coeff_inj {R : Type u} [semiring R] {p q : polynomial R} :
p.coeff = q.coeff p = q
theorem polynomial.to_finsupp_apply {R : Type u} [semiring R] (f : polynomial R) (i : ) :
theorem polynomial.coeff_monomial {R : Type u} {a : R} {m n : } [semiring R] :
( 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] :
= 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] :
.coeff n = ite (n = 0) a 0
@[simp]
theorem polynomial.coeff_C_zero {R : Type u} {a : R} [semiring R] :
.coeff 0 = a
theorem polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : } [semiring R] (h : n 0) :
.coeff n = 0
theorem polynomial.C_mul_X_pow_eq_monomial {R : Type u} {a : R} [semiring R] {n : } :
= a
@[simp]
theorem polynomial.to_finsupp_C_mul_X_pow {R : Type u} [semiring R] (a : R) (n : ) :
theorem polynomial.C_mul_X_eq_monomial {R : Type u} {a : R} [semiring R] :
@[simp]
theorem polynomial.to_finsupp_C_mul_X {R : Type u} [semiring R] (a : R) :
theorem polynomial.C_injective {R : Type u} [semiring R] :
@[simp]
theorem polynomial.C_inj {R : Type u} {a b : R} [semiring R] :
a = b
@[simp]
theorem polynomial.C_eq_zero {R : Type u} {a : R} [semiring R] :
a = 0
theorem polynomial.C_ne_zero {R : Type u} {a : R} [semiring R] :
a 0
theorem polynomial.nontrivial.of_polynomial_ne {R : Type u} [semiring R] {p q : polynomial R} (h : p q) :
theorem polynomial.forall_eq_iff_forall_eq {R : Type u} [semiring R] :
( (f g : , f = g) (a b : R), a = b
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

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 : →+ M} (h : (n : ) (a : R), f ( a) = g ( a)) :
f = g
@[ext]
theorem polynomial.add_hom_ext' {R : Type u} [semiring R] {M : Type u_1} [add_monoid M] {f g : →+ M} (h : (n : ), ) :
f = g
@[ext]
theorem polynomial.lhom_ext' {R : Type u} [semiring R] {M : Type u_1} [ M] {f g : →ₗ[R] M} (h : (n : ), f.comp = g.comp ) :
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) :
( a).support = {n}
theorem polynomial.support_monomial' {R : Type u} [semiring R] (n : ) (a : R) :
( a).support {n}
theorem polynomial.support_C_mul_X {R : Type u} [semiring R] {c : R} (h : c 0) :
= {1}
theorem polynomial.support_C_mul_X' {R : Type u} [semiring R] (c : R) :
{1}
theorem polynomial.support_C_mul_X_pow {R : Type u} [semiring R] (n : ) {c : R} (h : c 0) :
* .support = {n}
theorem polynomial.support_C_mul_X_pow' {R : Type u} [semiring R] (n : ) (c : R) :
* .support {n}
theorem polynomial.support_binomial' {R : Type u} [semiring R] (k m : ) (x y : R) :
+ .support {k, m}
theorem polynomial.support_trinomial' {R : Type u} [semiring R] (k m n : ) (x y z : R) :
+ + .support {k, m, n}
theorem polynomial.X_pow_eq_monomial {R : Type u} [semiring R] (n : ) :
= 1
@[simp]
theorem polynomial.to_finsupp_X_pow {R : Type u} [semiring R] (n : ) :
theorem polynomial.smul_X_eq_monomial {R : Type u} {a : R} [semiring R] {n : } :
a = a
theorem polynomial.support_X_pow {R : Type u} [semiring R] (H : ¬1 = 0) (n : ) :
.support = {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} [semiring R] {a : R} (ha : a 0) {i j : } :
a = a i = j
theorem polynomial.binomial_eq_binomial {R : Type u} [semiring R] {k l m n : } {u v : R} (hu : u 0) (hv : v 0) :
+ = + k = m l = n u = v k = n l = m u + v = 0 k = l m = n
theorem polynomial.nat_cast_mul {R : Type u} [semiring R] (n : ) (p : polynomial R) :
n * p = n p
def polynomial.sum {R : Type u} [semiring R] {S : Type u_1} (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} (p : polynomial R) (f : R S) :
p.sum f = p.support.sum (λ (n : ), f n (p.coeff n))
theorem polynomial.sum_eq_of_subset {R : Type u} [semiring R] {S : Type u_1} (p : polynomial R) (f : R S) (hf : (i : ), f i 0 = 0) (s : finset ) (hs : p.support s) :
p.sum f = s.sum (λ (n : ), f n (p.coeff n))
theorem polynomial.mul_eq_sum_sum {R : Type u} [semiring R] {p q : polynomial R} :
p * q = p.support.sum (λ (i : ), 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} (f : R S) :
0.sum f = 0
@[simp]
theorem polynomial.sum_monomial_index {R : Type u} [semiring R] {S : Type u_1} (n : ) (a : R) (f : R S) (hf : f n 0 = 0) :
( a).sum f = f n a
@[simp]
theorem polynomial.sum_C_index {R : Type u} [semiring R] {a : R} {β : Type u_1} {f : R β} (h : f 0 0 = 0) :
.sum f = f 0 a
@[simp]
theorem polynomial.sum_X_index {R : Type u} [semiring R] {S : Type u_1} {f : R S} (hf : f 1 0 = 0) :
= f 1 1
theorem polynomial.sum_add_index {R : Type u} [semiring R] {S : Type u_1} (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} (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} (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} (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))
theorem polynomial.sum_monomial_eq {R : Type u} [semiring R] (p : polynomial R) :
p.sum (λ (n : ) (a : R), a) = p
theorem polynomial.sum_C_mul_X_pow_eq {R : Type u} [semiring R] (p : polynomial R) :
p.sum (λ (n : ) (a : R), = p
@[irreducible]
noncomputable 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.to_finsupp_erase {R : Type u} [semiring R] (p : polynomial R) (n : ) :
@[simp]
theorem polynomial.of_finsupp_erase {R : Type u} [semiring R] (p : ) (n : ) :
{to_finsupp := p} = {to_finsupp := p}
@[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 : ) :
(p.coeff n) + = p
theorem polynomial.coeff_erase {R : Type u} [semiring R] (p : polynomial R) (n i : ) :
p).coeff i = ite (i = n) 0 (p.coeff i)
@[simp]
theorem polynomial.erase_zero {R : Type u} [semiring R] (n : ) :
= 0
@[simp]
theorem polynomial.erase_monomial {R : Type u} [semiring R] {n : } {a : R} :
( a) = 0
@[simp]
theorem polynomial.erase_same {R : Type u} [semiring R] (p : polynomial R) (n : ) :
p).coeff n = 0
@[simp]
theorem polynomial.erase_ne {R : Type u} [semiring R] (p : polynomial R) (n i : ) (h : i n) :
p).coeff i = p.coeff i
noncomputable def polynomial.update {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) :

Replace the coefficient of a `p : R[X]` 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
theorem polynomial.coeff_update {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) :
(p.update n a).coeff = a
theorem polynomial.coeff_update_apply {R : Type u} [semiring R] (p : polynomial R) (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 : polynomial R) (n : ) (a : R) :
(p.update n a).coeff n = a
theorem polynomial.coeff_update_ne {R : Type u} [semiring R] (p : polynomial R) {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 : polynomial R) (n : ) :
p.update n 0 =
theorem polynomial.support_update {R : Type u} [semiring R] (p : polynomial R) (n : ) (a : R) [decidable (a = 0)] :
(p.update n a).support = ite (a = 0) (p.support.erase n) p.support)
theorem polynomial.support_update_zero {R : Type u} [semiring R] (p : polynomial R) (n : ) :
theorem polynomial.support_update_ne_zero {R : Type u} [semiring R] (p : polynomial R) (n : ) {a : R} (ha : a 0) :
(p.update n a).support =
@[protected, instance]
noncomputable def polynomial.comm_semiring {R : Type u}  :
Equations
• polynomial.comm_semiring = 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 polynomial.comm_semiring._proof_8
@[protected, instance]
noncomputable def polynomial.has_int_cast {R : Type u} [ring R] :
Equations
@[protected, instance]
noncomputable 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) :
(-a) = - a
@[simp]
theorem polynomial.support_neg {R : Type u} [ring R] {p : polynomial R} :
@[simp]
theorem polynomial.C_eq_int_cast {R : Type u} [ring R] (n : ) :
@[protected, instance]
noncomputable def polynomial.comm_ring {R : Type u} [comm_ring R] :
Equations
• polynomial.comm_ring = 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 polynomial.comm_ring._proof_11 polynomial.comm_ring._proof_12
@[protected, instance]
theorem polynomial.X_ne_zero {R : Type u} [semiring R] [nontrivial R] :
theorem polynomial.rat_smul_eq_C_mul {R : Type u} (a : ) (f : polynomial R) :
a f =
@[simp]
theorem polynomial.nontrivial_iff {R : Type u} [semiring R] :
@[protected, instance]
noncomputable def polynomial.has_repr {R : Type u} [semiring R] [has_repr R] :
Equations