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 ∈ 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.
• ofMultiset s is the monic polynomial p which has roots s.

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 (fun 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 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 R[ℕ] is through a structure to make polynomials irreducible from the point of view of the kernel. Most operations are irreducible since Lean cannot compute anyway with AddMonoidAlgebra. 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 R[ℕ] is done through ofFinsupp and toFinsupp (or, equivalently, rcases p when p is a polynomial gives an element q of R[ℕ], and conversely ⟨q⟩ gives back p). The equivalence is also registered as a ring equiv in Polynomial.toFinsuppIso. These should in general not be used once the basic API for polynomials is constructed.

@[reducible, inline]

abbrev Polynomial (R : Type u_1) [Semiring R] : Type u_1

Polynomial R is the type of univariate polynomials over R, denoted as R[X] within the Polynomial namespace.

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

Equations

• Polynomial R = AddMonoidAlgebra R ℕ

def Polynomial.«term_[X]» : Lean.TrailingParserDescr

Polynomial R is the type of univariate polynomials over R, denoted as R[X] within the Polynomial namespace.

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

Equations

• Polynomial.«term_[X]» = Lean.ParserDescr.trailingNode `Polynomial.«term_[X]» 9000 0 (Lean.ParserDescr.symbol "[X]")

@[deprecated id (since := "2026-07-18")]

def Polynomial.toFinsupp {R : Type u} [Semiring R] : Polynomial R → AddMonoidAlgebra R ℕ

The underlying R[ℕ] of a polynomial in R[X]. Now the identity, as R[X] is defeq R[ℕ].

Equations

• Polynomial.toFinsupp = id

@[deprecated id (since := "2026-07-18")]

def Polynomial.ofFinsupp {R : Type u} [Semiring R] : AddMonoidAlgebra R ℕ → Polynomial R

Construct a polynomial in R[X] from an element of R[ℕ]. Now the identity, as R[X] is defeq R[ℕ].

Equations

• Polynomial.ofFinsupp = id

@[deprecated AddMonoidAlgebra.forall (since := "2026-09-11")]

theorem Polynomial.forall_iff_forall_finsupp {R : Type u} [Semiring R] (P : Polynomial R → Prop) : (∀ (p : Polynomial R), P p) ↔ ∀ (q : ℕ →₀ R), P (AddMonoidAlgebra.ofCoeff q)

@[deprecated AddMonoidAlgebra.exists (since := "2026-09-11")]

theorem Polynomial.exists_iff_exists_finsupp {R : Type u} [Semiring R] (P : Polynomial R → Prop) : (∃ (p : Polynomial R), P p) ↔ ∃ (q : ℕ →₀ R), P (AddMonoidAlgebra.ofCoeff q)

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.eta {R : Type u} [Semiring R] (f : Polynomial R) : ofFinsupp f.toFinsupp = f

Conversions to and from AddMonoidAlgebra

Since R[X] is not defeq to 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.ofFinsupp and Polynomial.toFinsupp.

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_zero {R : Type u} [Semiring R] : ofFinsupp 0 = 0

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_one {R : Type u} [Semiring R] : ofFinsupp 1 = 1

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_add {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} : ofFinsupp (a + b) = ofFinsupp a + ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_neg {R : Type u} [Ring R] {a : AddMonoidAlgebra R ℕ} : ofFinsupp (-a) = -ofFinsupp a

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_sub {R : Type u} [Ring R] {a b : AddMonoidAlgebra R ℕ} : ofFinsupp (a - b) = ofFinsupp a - ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_mul {R : Type u} [Semiring R] (a b : AddMonoidAlgebra R ℕ) : ofFinsupp (a * b) = ofFinsupp a * ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_nsmul {R : Type u} [Semiring R] (a : ℕ) (b : AddMonoidAlgebra R ℕ) : ofFinsupp (a • b) = a • ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : AddMonoidAlgebra R ℕ) : ofFinsupp (a • b) = a • ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_pow {R : Type u} [Semiring R] (a : AddMonoidAlgebra R ℕ) (n : ℕ) : ofFinsupp (a ^ n) = ofFinsupp a ^ n

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_zero {R : Type u} [Semiring R] : toFinsupp 0 = 0

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_one {R : Type u} [Semiring R] : toFinsupp 1 = 1

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_add {R : Type u} [Semiring R] (a b : Polynomial R) : (a + b).toFinsupp = a.toFinsupp + b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_neg {R : Type u} [Ring R] (a : Polynomial R) : (-a).toFinsupp = -a.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_sub {R : Type u} [Ring R] (a b : Polynomial R) : (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_mul {R : Type u} [Semiring R] (a b : Polynomial R) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_nsmul {R : Type u} [Semiring R] (a : ℕ) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_pow {R : Type u} [Semiring R] (a : Polynomial R) (n : ℕ) : (a ^ n).toFinsupp = a.toFinsupp ^ n

theorem IsSMulRegular.polynomial {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] {a : S} (ha : IsSMulRegular R a) : IsSMulRegular (Polynomial R) a

@[deprecated Function.injective_id (since := "2026-07-18")]

theorem Polynomial.toFinsupp_injective {R : Type u} [Semiring R] : Function.Injective toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_inj {R : Type u} [Semiring R] {a b : Polynomial R} : a.toFinsupp = b.toFinsupp ↔ a = b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_eq_zero {R : Type u} [Semiring R] {a : Polynomial R} : a.toFinsupp = 0 ↔ a = 0

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_eq_one {R : Type u} [Semiring R] {a : Polynomial R} : a.toFinsupp = 1 ↔ a = 1

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_inj {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} : ofFinsupp a = ofFinsupp b ↔ a = b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_eq_zero {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} : ofFinsupp a = 0 ↔ a = 0

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_eq_one {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} : ofFinsupp a = 1 ↔ a = 1

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_natCast {R : Type u} [Semiring R] (n : ℕ) : ofFinsupp ↑n = ↑n

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_natCast {R : Type u} [Semiring R] (n : ℕ) : (↑n).toFinsupp = ↑n

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : ofFinsupp (OfNat.ofNat n) = OfNat.ofNat n

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).toFinsupp = OfNat.ofNat n

@[deprecated "Now a tautology" (since := "2026-07-18")]

noncomputable def Polynomial.toFinsuppIso (R : Type u) [Semiring R] : Polynomial R ≃+* AddMonoidAlgebra R ℕ

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

Equations

• Polynomial.toFinsuppIso R = RingEquiv.refl (Polynomial R)

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsuppIso_apply (R : Type u) [Semiring R] (a : Polynomial R) : (toFinsuppIso R) a = a

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsuppIso_symm_apply (R : Type u) [Semiring R] (a : Polynomial R) : (toFinsuppIso R).symm a = a

@[deprecated "Now a tautology" (since := "2026-07-18")]

noncomputable def Polynomial.toFinsuppIsoLinear (R : Type u) [Semiring R] : Polynomial R ≃ₗ[R] AddMonoidAlgebra R ℕ

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

Equations

• Polynomial.toFinsuppIsoLinear R = LinearEquiv.refl R (Polynomial R)

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsuppIsoLinear_apply (R : Type u) [Semiring R] (x : Polynomial R) : (toFinsuppIsoLinear R) x = x

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsuppIsoLinear_symm_apply (R : Type u) [Semiring R] (a✝ : Polynomial R) : (toFinsuppIsoLinear R).symm a✝ = a✝

@[deprecated "Now a tautology" (since := "2026-10-25")]

theorem Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp {R : Type u} [Semiring R] (f : AddMonoidAlgebra R ℕ) : ((toFinsuppIsoLinear R).symm f).toFinsupp = f

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_sum {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → AddMonoidAlgebra R ℕ) : ofFinsupp (∑ i ∈ s, f i) = ∑ i ∈ s, ofFinsupp (f i)

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_sum {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R) : (∑ i ∈ s, f i).toFinsupp = ∑ i ∈ s, (f i).toFinsupp

def Polynomial.support {R : Type u} [Semiring R] (p : Polynomial R) : Finset ℕ

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

Equations

• p.support = p.coeff.support

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.support_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) : (ofFinsupp p).support = p.coeff.support

theorem Polynomial.support_ofCoeff {R : Type u} [Semiring R] (q : ℕ →₀ R) : support (AddMonoidAlgebra.ofCoeff q) = q.support

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.support_toFinsupp {R : Type u} [Semiring R] (p : Polynomial R) : p.toFinsupp.coeff.support = p.support

@[simp]

theorem Polynomial.support_zero {R : Type u} [Semiring R] : support 0 = ∅

@[simp]

theorem Polynomial.support_eq_empty {R : Type u} [Semiring R] {p : Polynomial R} : p.support = ∅ ↔ p = 0

@[simp]

theorem Polynomial.support_nonempty {R : Type u} [Semiring R] {p : Polynomial R} : p.support.Nonempty ↔ 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 : ℕ) : R →ₗ[R] Polynomial R

monomial s a is the monomial a * X^s

Equations

• Polynomial.monomial n = { toFun := fun (t : R) => AddMonoidAlgebra.single n t, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.coeff_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) : ((monomial n) r).coeff = Finsupp.single n r

@[deprecated Polynomial.coeff_monomial (since := "2026-07-18")]

theorem Polynomial.toFinsupp_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) : ((monomial n) r).toFinsupp = AddMonoidAlgebra.single n r

theorem Polynomial.single_eq_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) : AddMonoidAlgebra.single n r = (monomial n) r

@[deprecated Polynomial.single_eq_monomial (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_single {R : Type u} [Semiring R] (n : ℕ) (r : R) : ofFinsupp (AddMonoidAlgebra.single n r) = (monomial n) r

@[simp]

theorem Polynomial.monomial_zero_right {R : Type u} [Semiring R] (n : ℕ) : (monomial n) 0 = 0

theorem Polynomial.monomial_zero_one {R : Type u} [Semiring R] : (monomial 0) 1 = 1

theorem Polynomial.monomial_mul_monomial {R : Type u} [Semiring R] (n m : ℕ) (r s : R) : (monomial n) r * (monomial m) s = (monomial (n + m)) (r * s)

@[simp]

theorem Polynomial.monomial_pow {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (monomial n) r ^ k = (monomial (n * k)) (r ^ k)

theorem Polynomial.smul_monomial {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (n : ℕ) (b : R) : a • (monomial n) b = (monomial n) (a • b)

theorem Polynomial.monomial_injective {R : Type u} [Semiring R] (n : ℕ) : Function.Injective ⇑(monomial n)

@[simp]

theorem Polynomial.monomial_eq_zero_iff {R : Type u} [Semiring R] (t : R) (n : ℕ) : (monomial n) t = 0 ↔ t = 0

theorem Polynomial.monomial_eq_monomial_iff {R : Type u} [Semiring R] {m n : ℕ} {a b : R} : (monomial m) a = (monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0

theorem Polynomial.support_add {R : Type u} [Semiring R] {p q : Polynomial R} : (p + q).support ⊆ p.support ∪ q.support

noncomputable def Polynomial.C {R : Type u} [Semiring R] : R →+* Polynomial R

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

Equations

• Polynomial.C = { toFun := (Polynomial.monomial 0).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Polynomial.monomial_zero_left {R : Type u} [Semiring R] ⦃a : R⦄ : (monomial 0) a = C a

@[deprecated "Use `AddMonoidAlgebra.coeff` directly" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_C {R : Type u} [Semiring R] (a : R) : (C a).toFinsupp = AddMonoidAlgebra.single 0 a

theorem Polynomial.C_0 {R : Type u} [Semiring R] : C 0 = 0

theorem Polynomial.C_1 {R : Type u} [Semiring R] : C 1 = 1

theorem Polynomial.C_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : C (OfNat.ofNat n) = OfNat.ofNat n

theorem Polynomial.C_mul {R : Type u} {a b : R} [Semiring R] : C (a * b) = C a * C b

theorem Polynomial.C_add {R : Type u} {a b : R} [Semiring R] : C (a + b) = C a + C b

@[simp]

theorem Polynomial.smul_C {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (s : S) (r : R) : s • C r = C (s • r)

theorem Polynomial.C_pow {R : Type u} {a : R} {n : ℕ} [Semiring R] : C (a ^ n) = C a ^ n

theorem Polynomial.C_eq_natCast {R : Type u} [Semiring R] (n : ℕ) : C ↑n = ↑n

@[simp]

theorem Polynomial.C_mul_monomial {R : Type u} {a b : R} {n : ℕ} [Semiring R] : C a * (monomial n) b = (monomial n) (a * b)

@[simp]

theorem Polynomial.monomial_mul_C {R : Type u} {a b : R} {n : ℕ} [Semiring R] : (monomial n) a * C b = (monomial n) (a * b)

noncomputable def Polynomial.X {R : Type u} [Semiring R] : Polynomial 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] : (monomial 1) 1 = X

theorem Polynomial.monomial_one_right_eq_X_pow {R : Type u} [Semiring R] (n : ℕ) : (monomial n) 1 = X ^ n

theorem Polynomial.X_eq_single {R : Type u} [Semiring R] : X = AddMonoidAlgebra.single 1 1

@[deprecated Polynomial.X_eq_single (since := "2026-07-18")]

theorem Polynomial.toFinsupp_X {R : Type u} [Semiring R] : X.toFinsupp = AddMonoidAlgebra.single 1 1

theorem Polynomial.X_ne_C {R : Type u} [Semiring R] [Nontrivial R] (a : R) : X ≠ C a

theorem Polynomial.X_mul {R : Type u} [Semiring R] {p : Polynomial R} : X * p = p * X

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

theorem Polynomial.X_pow_mul {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} : X ^ n * p = p * X ^ n

@[simp]

theorem Polynomial.X_mul_C {R : Type u} [Semiring R] (r : R) : X * C r = C r * 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 : ℕ) : X ^ n * C r = C r * 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 : Polynomial R} {n : ℕ} : p * X ^ n * q = p * q * X ^ n

@[simp]

theorem Polynomial.X_pow_mul_assoc_C {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (r : R) : p * X ^ n * C r = p * C r * 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 : Polynomial R) : Commute X p

theorem Polynomial.commute_X_pow {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : Commute (X ^ n) p

@[simp]

theorem Polynomial.monomial_mul_X {R : Type u} [Semiring R] (n : ℕ) (r : R) : (monomial n) r * X = (monomial (n + 1)) r

@[simp]

theorem Polynomial.monomial_mul_X_pow {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) : (monomial n) r * X ^ k = (monomial (n + k)) r

@[simp]

theorem Polynomial.X_mul_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) : X * (monomial n) r = (monomial (n + 1)) r

@[simp]

theorem Polynomial.X_pow_mul_monomial {R : Type u} [Semiring R] (k n : ℕ) (r : R) : X ^ k * (monomial n) r = (monomial (n + k)) r

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.coeff_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) : (ofFinsupp p).coeff = p.coeff

@[deprecated AddMonoidAlgebra.coeff_injective (since := "2026-10-25")]

theorem Polynomial.coeff_injective {R : Type u} [Semiring R] : Function.Injective AddMonoidAlgebra.coeff

@[deprecated AddMonoidAlgebra.coeff_inj (since := "2026-10-25")]

theorem Polynomial.coeff_inj {R : Type u} [Semiring R] {p q : Polynomial R} : p.coeff = q.coeff ↔ p = q

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_apply {R : Type u} [Semiring R] (f : Polynomial R) (i : ℕ) : f.toFinsupp.coeff i = f.coeff i

@[deprecated Finsupp.finite_range (since := "2026-10-25")]

theorem Polynomial.finite_range_coeff {R : Type u} [Semiring R] (f : Polynomial R) : (Set.range ⇑f.coeff).Finite

theorem Polynomial.coeff_monomial_apply {R : Type u} {a : R} {m n : ℕ} [Semiring R] : ((monomial n) a).coeff m = if n = m then a else 0

theorem Polynomial.coeff_monomial_same {R : Type u} [Semiring R] (n : ℕ) (c : R) : ((monomial n) c).coeff n = c

theorem Polynomial.coeff_monomial_of_ne {R : Type u} [Semiring R] {m n : ℕ} (c : R) (h : m ≠ n) : ((monomial n) c).coeff m = 0

@[simp]

theorem Polynomial.coeff_zero {R : Type u} [Semiring R] (n : ℕ) : (AddMonoidAlgebra.coeff 0) n = 0

theorem Polynomial.coeff_one {R : Type u} [Semiring R] {n : ℕ} : (AddMonoidAlgebra.coeff 1) n = if n = 0 then 1 else 0

@[deprecated AddMonoidAlgebra.coeff_one_zero (since := "2026-10-25")]

theorem Polynomial.coeff_one_zero {R : Type u} [Semiring R] : (AddMonoidAlgebra.coeff 1) 0 = 1

@[simp]

theorem Polynomial.coeff_X_one {R : Type u} [Semiring R] : X.coeff 1 = 1

@[simp]

theorem Polynomial.coeff_X_zero {R : Type u} [Semiring R] : X.coeff 0 = 0

theorem Polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : ℕ} [Semiring R] : ((monomial (n + 1)) a).coeff 0 = 0

theorem Polynomial.coeff_X {R : Type u} {n : ℕ} [Semiring R] : X.coeff n = if 1 = n then 1 else 0

theorem Polynomial.coeff_X_of_ne_one {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 1) : X.coeff n = 0

@[simp]

theorem Polynomial.mem_support_iff {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} : n ∈ p.support ↔ p.coeff n ≠ 0

theorem Polynomial.notMem_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] : (C a).coeff n = if n = 0 then a else 0

@[simp]

theorem Polynomial.coeff_C_zero {R : Type u} {a : R} [Semiring R] : (C a).coeff 0 = a

theorem Polynomial.coeff_C_of_ne_zero {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) : (C a).coeff n = 0

@[deprecated Polynomial.coeff_C_of_ne_zero (since := "2026-05-20")]

theorem Polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) : (C a).coeff n = 0

Alias of Polynomial.coeff_C_of_ne_zero.

@[simp]

theorem Polynomial.coeff_C_succ {R : Type u} [Semiring R] {r : R} {n : ℕ} : (C r).coeff (n + 1) = 0

theorem Polynomial.coeff_natCast_ite {R : Type u} {m n : ℕ} [Semiring R] : (↑m).coeff n = ↑(if n = 0 then m else 0)

theorem Polynomial.coeff_ofNat_zero {R : Type u} [Semiring R] (a : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).coeff 0 = OfNat.ofNat a

theorem Polynomial.coeff_ofNat_succ {R : Type u} [Semiring R] (a n : ℕ) [a.AtLeastTwo] : (OfNat.ofNat a).coeff (n + 1) = 0

theorem Polynomial.C_mul_X_pow_eq_monomial {R : Type u} {a : R} [Semiring R] {n : ℕ} : C a * X ^ n = (monomial n) a

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ℕ) : (C a * X ^ n).toFinsupp = AddMonoidAlgebra.single n a

theorem Polynomial.C_mul_X_eq_monomial {R : Type u} {a : R} [Semiring R] : C a * X = (monomial 1) a

@[deprecated AddMonoidAlgebra.coeff_single (since := "2026-07-18")]

theorem Polynomial.toFinsupp_C_mul_X {R : Type u} [Semiring R] (a : R) : (C a * X).toFinsupp = AddMonoidAlgebra.single 1 a

theorem Polynomial.C_injective {R : Type u} [Semiring R] : Function.Injective ⇑C

@[simp]

theorem Polynomial.C_inj {R : Type u} {a b : R} [Semiring R] : C a = C b ↔ a = b

@[simp]

theorem Polynomial.C_eq_zero {R : Type u} {a : R} [Semiring R] : C a = 0 ↔ a = 0

theorem Polynomial.C_ne_zero {R : Type u} {a : R} [Semiring R] : C a ≠ 0 ↔ a ≠ 0

theorem Polynomial.subsingleton_iff_subsingleton {R : Type u} [Semiring R] : Subsingleton (Polynomial R) ↔ Subsingleton R

theorem Polynomial.Nontrivial.of_polynomial_ne {R : Type u} [Semiring R] {p q : Polynomial R} (h : p ≠ q) : Nontrivial R

theorem Polynomial.forall_eq_iff_forall_eq {R : Type u} [Semiring R] : (∀ (f g : Polynomial R), f = g) ↔ ∀ (a b : R), a = b

@[deprecated AddMonoidAlgebra.ext_iff (since := "2026-10-25")]

theorem Polynomial.ext_iff {R : Type u} [Semiring R] {p q : Polynomial R} : p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n

@[deprecated AddMonoidAlgebra.ext (since := "2026-10-25")]

theorem Polynomial.ext {R : Type u} [Semiring R] {p q : Polynomial R} : (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q

theorem Polynomial.addSubmonoid_closure_setOfPred_eq_monomial {R : Type u} [Semiring R] : AddSubmonoid.closure {p : Polynomial R | ∃ (n : ℕ) (a : R), p = (monomial n) a} = ⊤

Monomials generate the additive monoid of polynomials.

@[deprecated Polynomial.addSubmonoid_closure_setOfPred_eq_monomial (since := "2026-07-09")]

theorem Polynomial.addSubmonoid_closure_setOf_eq_monomial {R : Type u} [Semiring R] : AddSubmonoid.closure {p : Polynomial R | ∃ (n : ℕ) (a : R), p = (monomial n) a} = ⊤

Alias of Polynomial.addSubmonoid_closure_setOfPred_eq_monomial.

---

Monomials generate the additive monoid of polynomials.

theorem Polynomial.addHom_ext {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} (h : ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)) : f = g

theorem Polynomial.addHom_ext_iff {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} : f = g ↔ ∀ (n : ℕ) (a : R), f ((monomial n) a) = g ((monomial n) a)

theorem Polynomial.addHom_ext' {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} (h : ∀ (n : ℕ), f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom) : f = g

theorem Polynomial.addHom_ext'_iff {R : Type u} [Semiring R] {M : Type u_1} [AddZeroClass M] {f g : Polynomial R →+ M} : f = g ↔ ∀ (n : ℕ), f.comp (monomial n).toAddMonoidHom = g.comp (monomial n).toAddMonoidHom

theorem Polynomial.lhom_ext' {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {f g : Polynomial R →ₗ[R] M} (h : ∀ (n : ℕ), f ∘ₗ monomial n = g ∘ₗ monomial n) : f = g

theorem Polynomial.lhom_ext'_iff {R : Type u} [Semiring R] {M : Type u_1} [AddCommMonoid M] [Module R M] {f g : Polynomial R →ₗ[R] M} : f = g ↔ ∀ (n : ℕ), f ∘ₗ monomial n = g ∘ₗ monomial n

theorem Polynomial.eq_zero_of_eq_zero {R : Type u} [Semiring R] (h : 0 = 1) (p : Polynomial R) : p = 0

@[simp]

theorem Polynomial.support_monomial {R : Type u} [Semiring R] (n : ℕ) {a : R} (h : a ≠ 0) : ((monomial n) a).support = {n}

theorem Polynomial.support_monomial_subset {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((monomial n) a).support ⊆ {n}

@[deprecated Polynomial.support_monomial_subset (since := "2026-06-09")]

theorem Polynomial.support_monomial' {R : Type u} [Semiring R] (n : ℕ) (a : R) : ((monomial n) a).support ⊆ {n}

Alias of Polynomial.support_monomial_subset.

@[simp]

theorem Polynomial.support_C {R : Type u} [Semiring R] {a : R} (h : a ≠ 0) : (C a).support = {0}

theorem Polynomial.support_C_subset {R : Type u} [Semiring R] (a : R) : (C a).support ⊆ {0}

@[simp]

theorem Polynomial.support_C_mul_X {R : Type u} [Semiring R] {c : R} (h : c ≠ 0) : (C c * X).support = {1}

theorem Polynomial.support_C_mul_X_subset {R : Type u} [Semiring R] (c : R) : (C c * X).support ⊆ {1}

@[deprecated Polynomial.support_C_mul_X_subset (since := "2026-06-09")]

theorem Polynomial.support_C_mul_X' {R : Type u} [Semiring R] (c : R) : (C c * X).support ⊆ {1}

Alias of Polynomial.support_C_mul_X_subset.

@[simp]

theorem Polynomial.support_C_mul_X_pow {R : Type u} [Semiring R] (n : ℕ) {c : R} (h : c ≠ 0) : (C c * X ^ n).support = {n}

theorem Polynomial.support_C_mul_X_pow_subset {R : Type u} [Semiring R] (n : ℕ) (c : R) : (C c * X ^ n).support ⊆ {n}

@[deprecated Polynomial.support_C_mul_X_pow_subset (since := "2026-06-09")]

theorem Polynomial.support_C_mul_X_pow' {R : Type u} [Semiring R] (n : ℕ) (c : R) : (C c * X ^ n).support ⊆ {n}

Alias of Polynomial.support_C_mul_X_pow_subset.

theorem Polynomial.support_binomial_subset {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (C x * X ^ k + C y * X ^ m).support ⊆ {k, m}

@[deprecated Polynomial.support_binomial_subset (since := "2026-06-09")]

theorem Polynomial.support_binomial' {R : Type u} [Semiring R] (k m : ℕ) (x y : R) : (C x * X ^ k + C y * X ^ m).support ⊆ {k, m}

Alias of Polynomial.support_binomial_subset.

theorem Polynomial.support_trinomial_subset {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support ⊆ {k, m, n}

@[deprecated Polynomial.support_trinomial_subset (since := "2026-06-09")]

theorem Polynomial.support_trinomial' {R : Type u} [Semiring R] (k m n : ℕ) (x y z : R) : (C x * X ^ k + C y * X ^ m + C z * X ^ n).support ⊆ {k, m, n}

Alias of Polynomial.support_trinomial_subset.

theorem Polynomial.X_pow_eq_monomial {R : Type u} [Semiring R] (n : ℕ) : X ^ n = (monomial n) 1

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_X_pow {R : Type u} [Semiring R] (n : ℕ) : (X ^ n).toFinsupp = AddMonoidAlgebra.single n 1

theorem Polynomial.smul_X_eq_monomial {R : Type u} {a : R} [Semiring R] {n : ℕ} : a • X ^ n = (monomial n) a

@[simp]

theorem Polynomial.support_X_pow {R : Type u} [Semiring R] [Nontrivial R] (n : ℕ) : (X ^ n).support = {n}

theorem Polynomial.support_X_empty {R : Type u} [Semiring R] (H : 1 = 0) : X.support = ∅

@[simp]

theorem Polynomial.support_X {R : Type u} [Semiring R] [Nontrivial R] : X.support = {1}

theorem Polynomial.monomial_left_inj {R : Type u} [Semiring R] {a : R} (ha : a ≠ 0) {i j : ℕ} : (monomial i) a = (monomial j) 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) : C u * X ^ k + C v * X ^ l = C u * X ^ m + C v * X ^ n ↔ k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n

theorem Polynomial.natCast_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} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : S

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

Equations

• p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

theorem Polynomial.sum_def {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

theorem Polynomial.sum_eq_of_subset {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {p : Polynomial R} (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) {s : Finset ℕ} (hs : p.support ⊆ s) : p.sum f = ∑ n ∈ s, f n (p.coeff n)

theorem Polynomial.mul_eq_sum_sum {R : Type u} [Semiring R] {p q : Polynomial R} : p * q = ∑ i ∈ p.support, q.sum fun (j : ℕ) (a : R) => (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} [AddCommMonoid S] (f : ℕ → R → S) : sum 0 f = 0

@[simp]

theorem Polynomial.sum_monomial_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {n : ℕ} (a : R) (f : ℕ → R → S) (hf : f n 0 = 0) : ((monomial n) a).sum f = f n a

@[simp]

theorem Polynomial.sum_C_index {R : Type u} [Semiring R] {a : R} {β : Type u_1} [AddCommMonoid β] {f : ℕ → R → β} (h : f 0 0 = 0) : (C a).sum f = f 0 a

@[simp]

theorem Polynomial.sum_X_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] {f : ℕ → R → S} (hf : f 1 0 = 0) : X.sum f = f 1 1

theorem Polynomial.sum_add_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid 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

@[simp]

theorem Polynomial.sum_add' {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S) : p.sum (f + g) = p.sum f + p.sum g

See also Polynomial.sum_add.

@[simp]

theorem Polynomial.sum_add {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (f g : ℕ → R → S) : (p.sum fun (n : ℕ) (x : R) => f n x + g n x) = p.sum f + p.sum g

See also Polynomial.sum_add'.

theorem Polynomial.sum_smul_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (p : Polynomial R) (b : R) (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) : (b • p).sum f = p.sum fun (n : ℕ) (a : R) => f n (b * a)

See also Polynomial.sum_smul_index' for a version using smul on the RHS.

theorem Polynomial.sum_smul_index' {R : Type u} [Semiring R] {S : Type u_1} {T : Type u_2} [DistribSMul T R] [AddCommMonoid S] (p : Polynomial R) (b : T) (f : ℕ → R → S) (hf : ∀ (i : ℕ), f i 0 = 0) : (b • p).sum f = p.sum fun (n : ℕ) (a : R) => f n (b • a)

See also Polynomial.sum_smul_index for a version using multiplication on the RHS.

theorem Polynomial.smul_sum {R : Type u} [Semiring R] {S : Type u_1} {T : Type u_2} [AddCommMonoid S] [DistribSMul T S] (p : Polynomial R) (b : T) (f : ℕ → R → S) : b • p.sum f = p.sum fun (n : ℕ) (a : R) => b • f n a

@[simp]

theorem Polynomial.sum_monomial_eq {R : Type u} [Semiring R] (p : Polynomial R) : (p.sum fun (n : ℕ) (a : R) => (monomial n) a) = p

theorem Polynomial.sum_C_mul_X_pow_eq {R : Type u} [Semiring R] (p : Polynomial R) : (p.sum fun (n : ℕ) (a : R) => C a * X ^ n) = p

theorem Polynomial.induction_on {R : Type u} [Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R) (C : ∀ (a : R), motive (C a)) (add : ∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) (monomial : ∀ (n : ℕ) (a : R), motive (Polynomial.C a * X ^ n) → motive (Polynomial.C a * X ^ (n + 1))) : motive p

theorem Polynomial.induction_on' {R : Type u} [Semiring R] {motive : Polynomial R → Prop} (p : Polynomial R) (add : ∀ (p q : Polynomial R), motive p → motive q → motive (p + q)) (monomial : ∀ (n : ℕ) (a : R), motive ((monomial n) a)) : motive p

To prove something about polynomials, it suffices to show the condition is closed under taking sums, and it holds for monomials.

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : toFinsupp (AddMonoidAlgebra.erase n p) = AddMonoidAlgebra.erase n p.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_erase {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) (n : ℕ) : ofFinsupp (AddMonoidAlgebra.erase n p) = AddMonoidAlgebra.erase n (ofFinsupp p)

@[simp]

theorem Polynomial.support_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : support (AddMonoidAlgebra.erase n p) = p.support.erase n

theorem Polynomial.monomial_add_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (monomial n) (p.coeff n) + AddMonoidAlgebra.erase n p = p

theorem Polynomial.coeff_erase {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) : (AddMonoidAlgebra.erase n p).coeff i = if i = n then 0 else p.coeff i

@[deprecated AddMonoidAlgebra.erase_zero (since := "2026-10-25")]

theorem Polynomial.erase_zero {R : Type u} [Semiring R] (n : ℕ) : AddMonoidAlgebra.erase n 0 = 0

@[simp]

theorem Polynomial.erase_monomial {R : Type u} [Semiring R] {n : ℕ} {a : R} : AddMonoidAlgebra.erase n ((monomial n) a) = 0

@[deprecated Finsupp.erase_same (since := "2026-09-17")]

theorem Polynomial.erase_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (AddMonoidAlgebra.erase n p).coeff n = 0

@[deprecated Finsupp.erase_ne (since := "2026-09-17")]

theorem Polynomial.erase_ne {R : Type u} [Semiring R] (p : Polynomial R) {n i : ℕ} (h : i ≠ n) : (AddMonoidAlgebra.erase n p).coeff i = p.coeff i

theorem Polynomial.coeff_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : ⇑(AddMonoidAlgebra.update n a p).coeff = Function.update (⇑p.coeff) n a

theorem Polynomial.coeff_update_apply {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ) : (AddMonoidAlgebra.update n a p).coeff i = if i = n then a else p.coeff i

@[deprecated Function.update_self (since := "2026-09-17")]

theorem Polynomial.coeff_update_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) : (AddMonoidAlgebra.update n a p).coeff n = a

theorem Polynomial.coeff_update_ne {R : Type u} [Semiring R] (p : Polynomial R) {n i : ℕ} (a : R) (h : i ≠ n) : (AddMonoidAlgebra.update n a p).coeff i = p.coeff i

@[simp]

theorem Polynomial.update_zero_eq_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : AddMonoidAlgebra.update n 0 p = AddMonoidAlgebra.erase n p

theorem Polynomial.support_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) [Decidable (a = 0)] : support (AddMonoidAlgebra.update n a p) = if a = 0 then p.support.erase n else insert n p.support

theorem Polynomial.support_update_zero {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : support (AddMonoidAlgebra.update n 0 p) = p.support.erase n

theorem Polynomial.support_update_ne_zero {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) {a : R} (ha : a ≠ 0) : support (AddMonoidAlgebra.update n a p) = insert n p.support

noncomputable def Polynomial.coeffs {R : Type u} [Semiring R] (p : Polynomial R) : Finset R

The finset of nonzero coefficients of a polynomial.

Equations

• p.coeffs = Finset.image (fun (n : ℕ) => p.coeff n) p.support

@[simp]

theorem Polynomial.coeffs_zero {R : Type u} [Semiring R] : coeffs 0 = ∅

theorem Polynomial.mem_coeffs_iff {R : Type u} [Semiring R] {p : Polynomial R} {c : R} : c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = p.coeff n

theorem Polynomial.coe_coeffs_subset_iff {R : Type u} [Semiring R] {p : Polynomial R} {s : Set R} : ↑p.coeffs ⊆ s ↔ ∀ (n : ℕ), p.coeff n ≠ 0 → p.coeff n ∈ s

theorem Polynomial.coeffs_subset_iff {R : Type u} [Semiring R] {p : Polynomial R} {s : Finset R} : p.coeffs ⊆ s ↔ ∀ (n : ℕ), p.coeff n ≠ 0 → p.coeff n ∈ s

theorem Polynomial.coeffs_one {R : Type u} [Semiring R] : coeffs 1 ⊆ {1}

theorem Polynomial.coeff_mem_coeffs {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.coeff n ≠ 0) : p.coeff n ∈ p.coeffs

@[simp]

theorem Polynomial.coeffs_empty_iff {R : Type u} [Semiring R] {p : Polynomial R} : p.coeffs = ∅ ↔ p = 0

@[simp]

theorem Polynomial.coeffs_nonempty_iff {R : Type u} [Semiring R] {p : Polynomial R} : p.coeffs.Nonempty ↔ p ≠ 0

theorem Polynomial.coeffs_monomial {R : Type u} [Semiring R] (n : ℕ) {c : R} (hc : c ≠ 0) : ((monomial n) c).coeffs = {c}

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_zsmul {R : Type u} [Ring R] (a : ℤ) (b : AddMonoidAlgebra R ℕ) : ofFinsupp (a • b) = a • ofFinsupp b

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_zsmul {R : Type u} [Ring R] (a : ℤ) (b : Polynomial R) : (a • b).toFinsupp = a • b.toFinsupp

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.ofFinsupp_intCast {R : Type u} [Ring R] (z : ℤ) : ofFinsupp ↑z = ↑z

@[deprecated "Now a tautology" (since := "2026-07-18")]

theorem Polynomial.toFinsupp_intCast {R : Type u} [Ring R] (z : ℤ) : (↑z).toFinsupp = ↑z

@[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) : (monomial n) (-a) = -(monomial n) a

theorem Polynomial.monomial_sub {R : Type u} {a b : R} [Ring R] (n : ℕ) : (monomial n) (a - b) = (monomial n) a - (monomial n) b

@[simp]

theorem Polynomial.support_neg {R : Type u} [Ring R] {p : Polynomial R} : (-p).support = p.support

theorem Polynomial.C_eq_intCast {R : Type u} [Ring R] (n : ℤ) : C ↑n = ↑n

theorem Polynomial.C_neg {R : Type u} {a : R} [Ring R] : C (-a) = -C a

theorem Polynomial.C_sub {R : Type u} {a b : R} [Ring R] : C (a - b) = C a - C b

@[simp]

theorem Polynomial.X_ne_zero {R : Type u} [Semiring R] [Nontrivial R] : X ≠ 0

theorem Polynomial.noZeroDivisors_iff {R : Type u} [Semiring R] : NoZeroDivisors (Polynomial R) ↔ NoZeroDivisors R

See also Polynomial.isCancelMulZero_iff: in order for R[X] to have cancellative multiplication (stronger than NoZeroDivisors in general, but equivalent if R is a ring), R must have both cancellative multiplication and cancellative addition.

theorem Polynomial.nnqsmul_eq_C_mul {R : Type u} [DivisionSemiring R] (q : ℚ≥0) (f : Polynomial R) : q • f = C ↑q * f

theorem Polynomial.qsmul_eq_C_mul {R : Type u} [DivisionRing R] (a : ℚ) (f : Polynomial R) : a • f = C ↑a * f

@[simp]

theorem Polynomial.nontrivial_iff {R : Type u} [Semiring R] : Nontrivial (Polynomial R) ↔ Nontrivial R

noncomputable def Polynomial.ofMultiset {R : Type u} [CommRing R] : AddChar (Multiset R) (Polynomial R)

The map sending a collection of roots into a polynomial, as a morphism.

Equations

• Polynomial.ofMultiset = { toFun := fun (s : Multiset R) => (Multiset.map (fun (a : R) => Polynomial.X - Polynomial.C a) s).prod, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }

@[simp]

theorem Polynomial.ofMultiset_apply {R : Type u} [CommRing R] (s : Multiset R) : ofMultiset s = (Multiset.map (fun (a : R) => X - C a) s).prod

@[instance_reducible]

instance Polynomial.repr {R : Type u} [Semiring R] [Repr R] [DecidableEq R] : Repr (Polynomial R)

Equations

• One or more equations did not get rendered due to their size.