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

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.

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

- ofFinsupp :: (

- toFinsupp : AddMonoidAlgebra R ℕ

  The coefficients `ℕ →₀ R` of a polynomial in `R[X]`.

- )

Instances For

source
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]")

Instances For

source
theorem Polynomial.forall_iff_forall_finsupp {R : Type u} [Semiring R] (P : Polynomial R → Prop) :
(∀ (p : Polynomial R), P p) ↔ ∀ (q : AddMonoidAlgebra R ℕ), P { toFinsupp := q }
source
theorem Polynomial.exists_iff_exists_finsupp {R : Type u} [Semiring R] (P : Polynomial R → Prop) :
(∃ (p : Polynomial R), P p) ↔ ∃ (q : AddMonoidAlgebra R ℕ), P { toFinsupp := q }
source
@[simp]
theorem Polynomial.eta {R : Type u} [Semiring R] (f : Polynomial R) :
{ toFinsupp := 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`.

source
instance Polynomial.zero {R : Type u} [Semiring R] :
Zero (Polynomial R)
Equations

- Polynomial.zero = { zero := { toFinsupp := 0 } }

source
instance Polynomial.one {R : Type u} [Semiring R] :
One (Polynomial R)
Equations

- Polynomial.one = { one := { toFinsupp := 1 } }

source
instance Polynomial.add' {R : Type u} [Semiring R] :
Add (Polynomial R)
Equations

- Polynomial.add' = { add := Polynomial.add✝ }

source
instance Polynomial.neg' {R : Type u} [Ring R] :
Neg (Polynomial R)
Equations

- Polynomial.neg' = { neg := Polynomial.neg✝ }

source
instance Polynomial.sub {R : Type u} [Ring R] :
Sub (Polynomial R)
Equations

- Polynomial.sub = { sub := fun (a b : Polynomial R) => a + -b }

source
instance Polynomial.mul' {R : Type u} [Semiring R] :
Mul (Polynomial R)
Equations

- Polynomial.mul' = { mul := Polynomial.mul✝ }

source
@[simp]
theorem Polynomial.add_eq_add {R : Type u} [Semiring R] {p q : Polynomial R} :
Polynomial.add✝ p q = p + q
source
@[simp]
theorem Polynomial.mul_eq_mul {R : Type u} [Semiring R] {p q : Polynomial R} :
Polynomial.mul✝ p q = p * q
source
instance Polynomial.instNSMul {R : Type u} [Semiring R] :
SMul ℕ (Polynomial R)
Equations

- Polynomial.instNSMul = { smul := fun (r : ℕ) (p : Polynomial R) => { toFinsupp := r • p.toFinsupp } }

source
instance Polynomial.smulZeroClass {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] :
SMulZeroClass S (Polynomial R)
Equations

- Polynomial.smulZeroClass = { smul := fun (r : S) (p : Polynomial R) => { toFinsupp := r • p.toFinsupp }, smul_zero := ⋯ }

source
instance Polynomial.instNoZeroSMulDivisors {R : Type u} [Semiring R] {S : Type u_1} [Zero S] [SMulZeroClass S R] [NoZeroSMulDivisors S R] :
NoZeroSMulDivisors S (Polynomial R)
source
@[instance 1]
instance Polynomial.pow {R : Type u} [Semiring R] :
Pow (Polynomial R) ℕ
Equations

- Polynomial.pow = { pow := fun (p : Polynomial R) (n : ℕ) => npowRec n p }

source
@[simp]
theorem Polynomial.ofFinsupp_zero {R : Type u} [Semiring R] :
{ toFinsupp := 0 } = 0
source
@[simp]
theorem Polynomial.ofFinsupp_one {R : Type u} [Semiring R] :
{ toFinsupp := 1 } = 1
source
@[simp]
theorem Polynomial.ofFinsupp_add {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} :
{ toFinsupp := a + b } = { toFinsupp := a } + { toFinsupp := b }
source
@[simp]
theorem Polynomial.ofFinsupp_neg {R : Type u} [Ring R] {a : AddMonoidAlgebra R ℕ} :
{ toFinsupp := -a } = -{ toFinsupp := a }
source
@[simp]
theorem Polynomial.ofFinsupp_sub {R : Type u} [Ring R] {a b : AddMonoidAlgebra R ℕ} :
{ toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
source
@[simp]
theorem Polynomial.ofFinsupp_mul {R : Type u} [Semiring R] (a b : AddMonoidAlgebra R ℕ) :
{ toFinsupp := a * b } = { toFinsupp := a } * { toFinsupp := b }
source
@[simp]
theorem Polynomial.ofFinsupp_nsmul {R : Type u} [Semiring R] (a : ℕ) (b : AddMonoidAlgebra R ℕ) :
{ toFinsupp := a • b } = a • { toFinsupp := b }
source
@[simp]
theorem Polynomial.ofFinsupp_smul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] (a : S) (b : AddMonoidAlgebra R ℕ) :
{ toFinsupp := a • b } = a • { toFinsupp := b }
source
@[simp]
theorem Polynomial.ofFinsupp_pow {R : Type u} [Semiring R] (a : AddMonoidAlgebra R ℕ) (n : ℕ) :
{ toFinsupp := a ^ n } = { toFinsupp := a } ^ n
source
@[simp]
theorem Polynomial.toFinsupp_zero {R : Type u} [Semiring R] :
toFinsupp 0 = 0
source
@[simp]
theorem Polynomial.toFinsupp_one {R : Type u} [Semiring R] :
toFinsupp 1 = 1
source
@[simp]
theorem Polynomial.toFinsupp_add {R : Type u} [Semiring R] (a b : Polynomial R) :
(a + b).toFinsupp = a.toFinsupp + b.toFinsupp
source
@[simp]
theorem Polynomial.toFinsupp_neg {R : Type u} [Ring R] (a : Polynomial R) :
(-a).toFinsupp = -a.toFinsupp
source
@[simp]
theorem Polynomial.toFinsupp_sub {R : Type u} [Ring R] (a b : Polynomial R) :
(a - b).toFinsupp = a.toFinsupp - b.toFinsupp
source
@[simp]
theorem Polynomial.toFinsupp_mul {R : Type u} [Semiring R] (a b : Polynomial R) :
(a * b).toFinsupp = a.toFinsupp * b.toFinsupp
source
@[simp]
theorem Polynomial.toFinsupp_nsmul {R : Type u} [Semiring R] (a : ℕ) (b : Polynomial R) :
(a • b).toFinsupp = a • b.toFinsupp
source
@[simp]
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
source
@[simp]
theorem Polynomial.toFinsupp_pow {R : Type u} [Semiring R] (a : Polynomial R) (n : ℕ) :
(a ^ n).toFinsupp = a.toFinsupp ^ n
source
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
source
theorem Polynomial.toFinsupp_injective {R : Type u} [Semiring R] :
Function.Injective toFinsupp
source
@[simp]
theorem Polynomial.toFinsupp_inj {R : Type u} [Semiring R] {a b : Polynomial R} :
a.toFinsupp = b.toFinsupp ↔ a = b
source
@[simp]
theorem Polynomial.toFinsupp_eq_zero {R : Type u} [Semiring R] {a : Polynomial R} :
a.toFinsupp = 0 ↔ a = 0
source
@[simp]
theorem Polynomial.toFinsupp_eq_one {R : Type u} [Semiring R] {a : Polynomial R} :
a.toFinsupp = 1 ↔ a = 1
source
theorem Polynomial.ofFinsupp_inj {R : Type u} [Semiring R] {a b : AddMonoidAlgebra R ℕ} :
{ toFinsupp := a } = { toFinsupp := b } ↔ a = b

A more convenient spelling of `Polynomial.ofFinsupp.injEq` in terms of `Iff`.

source
@[simp]
theorem Polynomial.ofFinsupp_eq_zero {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} :
{ toFinsupp := a } = 0 ↔ a = 0
source
@[simp]
theorem Polynomial.ofFinsupp_eq_one {R : Type u} [Semiring R] {a : AddMonoidAlgebra R ℕ} :
{ toFinsupp := a } = 1 ↔ a = 1
source
instance Polynomial.inhabited {R : Type u} [Semiring R] :
Inhabited (Polynomial R)
Equations

- Polynomial.inhabited = { default := 0 }

source
instance Polynomial.instNatCast {R : Type u} [Semiring R] :
NatCast (Polynomial R)
Equations

- Polynomial.instNatCast = { natCast := fun (n : ℕ) => { toFinsupp := ↑n } }

source
@[simp]
theorem Polynomial.ofFinsupp_natCast {R : Type u} [Semiring R] (n : ℕ) :
{ toFinsupp := ↑n } = ↑n
source
@[simp]
theorem Polynomial.toFinsupp_natCast {R : Type u} [Semiring R] (n : ℕ) :
(↑n).toFinsupp = ↑n
source
@[simp]
theorem Polynomial.ofFinsupp_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] :
{ toFinsupp := OfNat.ofNat n } = OfNat.ofNat n
source
@[simp]
theorem Polynomial.toFinsupp_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).toFinsupp = OfNat.ofNat n
source
instance Polynomial.semiring {R : Type u} [Semiring R] :
Semiring (Polynomial R)
Equations

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

source
instance Polynomial.distribSMul {R : Type u} [Semiring R] {S : Type u_1} [DistribSMul S R] :
DistribSMul S (Polynomial R)
Equations

- Polynomial.distribSMul = { toSMulZeroClass := Polynomial.smulZeroClass, smul_add := ⋯ }

source
instance Polynomial.distribMulAction {R : Type u} [Semiring R] {S : Type u_1} [Monoid S] [DistribMulAction S R] :
DistribMulAction S (Polynomial R)
Equations

- Polynomial.distribMulAction = { toSMul := Polynomial.smulZeroClass.toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

source
instance Polynomial.faithfulSMul {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [FaithfulSMul S R] :
FaithfulSMul S (Polynomial R)
source
instance Polynomial.module {R : Type u} [Semiring R] {S : Type u_1} [Semiring S] [Module S R] :
Module S (Polynomial R)
Equations

- Polynomial.module = { toDistribMulAction := Polynomial.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

source
instance Polynomial.smulCommClass {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [SMulCommClass S₁ S₂ R] :
SMulCommClass S₁ S₂ (Polynomial R)
source
instance Polynomial.isScalarTower {R : Type u} [Semiring R] {S₁ : Type u_1} {S₂ : Type u_2} [SMul S₁ S₂] [SMulZeroClass S₁ R] [SMulZeroClass S₂ R] [IsScalarTower S₁ S₂ R] :
IsScalarTower S₁ S₂ (Polynomial R)
source
instance Polynomial.isScalarTower_right {α : Type u_1} {K : Type u_2} [Semiring K] [DistribSMul α K] [IsScalarTower α K K] :
IsScalarTower α (Polynomial K) (Polynomial K)
source
instance Polynomial.isCentralScalar {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [SMulZeroClass S ᵐᵒᵖ R] [IsCentralScalar S R] :
IsCentralScalar S (Polynomial R)
source
instance Polynomial.unique {R : Type u} [Semiring R] [Subsingleton R] :
Unique (Polynomial R)
Equations

- Polynomial.unique = { toInhabited := Polynomial.inhabited, uniq := ⋯ }

source
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 = { toFun := Polynomial.toFinsupp, invFun := Polynomial.ofFinsupp, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.toFinsuppIso_apply (R : Type u) [Semiring R] (self : Polynomial R) :
(toFinsuppIso R) self = self.toFinsupp
source
@[simp]
theorem Polynomial.toFinsuppIso_symm_apply (R : Type u) [Semiring R] (toFinsupp : AddMonoidAlgebra R ℕ) :
(toFinsuppIso R).symm toFinsupp = { toFinsupp := toFinsupp }
source
instance Polynomial.instDecidableEq (R : Type u) [Semiring R] [DecidableEq R] :
DecidableEq (Polynomial R)
Equations

- Polynomial.instDecidableEq R = (Polynomial.toFinsuppIso R).decidableEq

source
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 = { toFun := (Polynomial.toFinsuppIso R).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Polynomial.toFinsuppIso R).invFun, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.toFinsuppIsoLinear_symm_apply_toFinsupp (R : Type u) [Semiring R] (a✝ : AddMonoidAlgebra R ℕ) :
((toFinsuppIsoLinear R).symm a✝).toFinsupp = a✝
source
@[simp]
theorem Polynomial.toFinsuppIsoLinear_apply (R : Type u) [Semiring R] (a✝ : Polynomial R) :
(toFinsuppIsoLinear R) a✝ = a✝.toFinsupp
source
theorem Polynomial.ofFinsupp_sum {R : Type u} [Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → AddMonoidAlgebra R ℕ) :
{ toFinsupp := ∑ i ∈ s, f i } = ∑ i ∈ s, { toFinsupp := f i }
source
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
source
def Polynomial.support {R : Type u} [Semiring R] :
Polynomial R → Finset ℕ

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

Equations

- { toFinsupp := p }.support = p.support

Instances For

source
@[simp]
theorem Polynomial.support_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) :
{ toFinsupp := p }.support = p.support
source
theorem Polynomial.support_toFinsupp {R : Type u} [Semiring R] (p : Polynomial R) :
p.toFinsupp.support = p.support
source
@[simp]
theorem Polynomial.support_zero {R : Type u} [Semiring R] :
support 0 = ∅
source
@[simp]
theorem Polynomial.support_eq_empty {R : Type u} [Semiring R] {p : Polynomial R} :
p.support = ∅ ↔ p = 0
source
@[simp]
theorem Polynomial.support_nonempty {R : Type u} [Semiring R] {p : Polynomial R} :
p.support.Nonempty ↔ p ≠ 0
source
theorem Polynomial.card_support_eq_zero {R : Type u} [Semiring R] {p : Polynomial R} :
p.support.card = 0 ↔ p = 0
source
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) => { toFinsupp := Finsupp.single n t }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.toFinsupp_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) :
((monomial n) r).toFinsupp = Finsupp.single n r
source
@[simp]
theorem Polynomial.ofFinsupp_single {R : Type u} [Semiring R] (n : ℕ) (r : R) :
{ toFinsupp := Finsupp.single n r } = (monomial n) r
source
@[simp]
theorem Polynomial.monomial_zero_right {R : Type u} [Semiring R] (n : ℕ) :
(monomial n) 0 = 0
source
theorem Polynomial.monomial_zero_one {R : Type u} [Semiring R] :
(monomial 0) 1 = 1
source
theorem Polynomial.monomial_add {R : Type u} [Semiring R] (n : ℕ) (r s : R) :
(monomial n) (r + s) = (monomial n) r + (monomial n) s
source
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)
source
@[simp]
theorem Polynomial.monomial_pow {R : Type u} [Semiring R] (n : ℕ) (r : R) (k : ℕ) :
(monomial n) r ^ k = (monomial (n * k)) (r ^ k)
source
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)
source
theorem Polynomial.monomial_injective {R : Type u} [Semiring R] (n : ℕ) :
Function.Injective ⇑(monomial n)
source
@[simp]
theorem Polynomial.monomial_eq_zero_iff {R : Type u} [Semiring R] (t : R) (n : ℕ) :
(monomial n) t = 0 ↔ t = 0
source
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
source
theorem Polynomial.support_add {R : Type u} [Semiring R] {p q : Polynomial R} :
(p + q).support ⊆ p.support ∪ q.support
source
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' := ⋯ }

Instances For

source
@[simp]
theorem Polynomial.monomial_zero_left {R : Type u} [Semiring R] (a : R) :
(monomial 0) a = C a
source
@[simp]
theorem Polynomial.toFinsupp_C {R : Type u} [Semiring R] (a : R) :
(C a).toFinsupp = AddMonoidAlgebra.single 0 a
source
theorem Polynomial.C_0 {R : Type u} [Semiring R] :
C 0 = 0
source
theorem Polynomial.C_1 {R : Type u} [Semiring R] :
C 1 = 1
source
theorem Polynomial.C_ofNat {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] :
C (OfNat.ofNat n) = OfNat.ofNat n
source
theorem Polynomial.C_mul {R : Type u} {a b : R} [Semiring R] :
C (a * b) = C a * C b
source
theorem Polynomial.C_add {R : Type u} {a b : R} [Semiring R] :
C (a + b) = C a + C b
source
@[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)
source
theorem Polynomial.C_pow {R : Type u} {a : R} {n : ℕ} [Semiring R] :
C (a ^ n) = C a ^ n
source
theorem Polynomial.C_eq_natCast {R : Type u} [Semiring R] (n : ℕ) :
C ↑n = ↑n
source
@[simp]
theorem Polynomial.C_mul_monomial {R : Type u} {a b : R} {n : ℕ} [Semiring R] :
C a * (monomial n) b = (monomial n) (a * b)
source
@[simp]
theorem Polynomial.monomial_mul_C {R : Type u} {a b : R} {n : ℕ} [Semiring R] :
(monomial n) a * C b = (monomial n) (a * b)
source
def Polynomial.X {R : Type u} [Semiring R] :
Polynomial R

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

Equations

- Polynomial.X = (Polynomial.monomial 1) 1

Instances For

source
theorem Polynomial.monomial_one_one_eq_X {R : Type u} [Semiring R] :
(monomial 1) 1 = X
source
theorem Polynomial.monomial_one_right_eq_X_pow {R : Type u} [Semiring R] (n : ℕ) :
(monomial n) 1 = X ^ n
source
@[simp]
theorem Polynomial.toFinsupp_X {R : Type u} [Semiring R] :
X.toFinsupp = Finsupp.single 1 1
source
theorem Polynomial.X_ne_C {R : Type u} [Semiring R] [Nontrivial R] (a : R) :
X ≠ C a
source
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.

source
theorem Polynomial.X_pow_mul {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} :
X ^ n * p = p * X ^ n
source
@[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`.

source
@[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`.

source
theorem Polynomial.X_pow_mul_assoc {R : Type u} [Semiring R] {p q : Polynomial R} {n : ℕ} :
p * X ^ n * q = p * q * X ^ n
source
@[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`.

source
theorem Polynomial.commute_X {R : Type u} [Semiring R] (p : Polynomial R) :
Commute X p
source
theorem Polynomial.commute_X_pow {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
Commute (X ^ n) p
source
@[simp]
theorem Polynomial.monomial_mul_X {R : Type u} [Semiring R] (n : ℕ) (r : R) :
(monomial n) r * X = (monomial (n + 1)) r
source
@[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
source
@[simp]
theorem Polynomial.X_mul_monomial {R : Type u} [Semiring R] (n : ℕ) (r : R) :
X * (monomial n) r = (monomial (n + 1)) r
source
@[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
source
def Polynomial.coeff {R : Type u} [Semiring R] :
Polynomial R → ℕ → R

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

Equations

- { toFinsupp := p }.coeff = ⇑p

Instances For

source
@[simp]
theorem Polynomial.coeff_ofFinsupp {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) :
{ toFinsupp := p }.coeff = ⇑p
source
theorem Polynomial.coeff_injective {R : Type u} [Semiring R] :
Function.Injective coeff
source
@[simp]
theorem Polynomial.coeff_inj {R : Type u} [Semiring R] {p q : Polynomial R} :
p.coeff = q.coeff ↔ p = q
source
theorem Polynomial.toFinsupp_apply {R : Type u} [Semiring R] (f : Polynomial R) (i : ℕ) :
f.toFinsupp i = f.coeff i
source
theorem Polynomial.coeff_monomial {R : Type u} {a : R} {m n : ℕ} [Semiring R] :
((monomial n) a).coeff m = if n = m then a else 0
source
@[simp]
theorem Polynomial.coeff_monomial_same {R : Type u} [Semiring R] (n : ℕ) (c : R) :
((monomial n) c).coeff n = c
source
theorem Polynomial.coeff_monomial_of_ne {R : Type u} [Semiring R] {m n : ℕ} (c : R) (h : m ≠ n) :
((monomial n) c).coeff m = 0
source
@[simp]
theorem Polynomial.coeff_zero {R : Type u} [Semiring R] (n : ℕ) :
coeff 0 n = 0
source
theorem Polynomial.coeff_one {R : Type u} [Semiring R] {n : ℕ} :
coeff 1 n = if n = 0 then 1 else 0
source
@[simp]
theorem Polynomial.coeff_one_zero {R : Type u} [Semiring R] :
coeff 1 0 = 1
source
@[simp]
theorem Polynomial.coeff_X_one {R : Type u} [Semiring R] :
X.coeff 1 = 1
source
@[simp]
theorem Polynomial.coeff_X_zero {R : Type u} [Semiring R] :
X.coeff 0 = 0
source
@[simp]
theorem Polynomial.coeff_monomial_succ {R : Type u} {a : R} {n : ℕ} [Semiring R] :
((monomial (n + 1)) a).coeff 0 = 0
source
theorem Polynomial.coeff_X {R : Type u} {n : ℕ} [Semiring R] :
X.coeff n = if 1 = n then 1 else 0
source
theorem Polynomial.coeff_X_of_ne_one {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 1) :
X.coeff n = 0
source
@[simp]
theorem Polynomial.mem_support_iff {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} :
n ∈ p.support ↔ p.coeff n ≠ 0
source
theorem Polynomial.notMem_support_iff {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} :
n ∉ p.support ↔ p.coeff n = 0
source
@[deprecated Polynomial.notMem_support_iff (since := "2025-05-23")]
theorem Polynomial.not_mem_support_iff {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} :
n ∉ p.support ↔ p.coeff n = 0

Alias of `Polynomial.notMem_support_iff`.

source
theorem Polynomial.coeff_C {R : Type u} {a : R} {n : ℕ} [Semiring R] :
(C a).coeff n = if n = 0 then a else 0
source
@[simp]
theorem Polynomial.coeff_C_zero {R : Type u} {a : R} [Semiring R] :
(C a).coeff 0 = a
source
theorem Polynomial.coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [Semiring R] (h : n ≠ 0) :
(C a).coeff n = 0
source
@[simp]
theorem Polynomial.coeff_C_succ {R : Type u} [Semiring R] {r : R} {n : ℕ} :
(C r).coeff (n + 1) = 0
source
@[simp]
theorem Polynomial.coeff_natCast_ite {R : Type u} {m n : ℕ} [Semiring R] :
(↑m).coeff n = ↑(if n = 0 then m else 0)
source
@[simp]
theorem Polynomial.coeff_ofNat_zero {R : Type u} [Semiring R] (a : ℕ) [a.AtLeastTwo] :
(OfNat.ofNat a).coeff 0 = OfNat.ofNat a
source
@[simp]
theorem Polynomial.coeff_ofNat_succ {R : Type u} [Semiring R] (a n : ℕ) [h : a.AtLeastTwo] :
(OfNat.ofNat a).coeff (n + 1) = 0
source
theorem Polynomial.C_mul_X_pow_eq_monomial {R : Type u} {a : R} [Semiring R] {n : ℕ} :
C a * X ^ n = (monomial n) a
source
@[simp]
theorem Polynomial.toFinsupp_C_mul_X_pow {R : Type u} [Semiring R] (a : R) (n : ℕ) :
(C a * X ^ n).toFinsupp = Finsupp.single n a
source
theorem Polynomial.C_mul_X_eq_monomial {R : Type u} {a : R} [Semiring R] :
C a * X = (monomial 1) a
source
@[simp]
theorem Polynomial.toFinsupp_C_mul_X {R : Type u} [Semiring R] (a : R) :
(C a * X).toFinsupp = Finsupp.single 1 a
source
theorem Polynomial.C_injective {R : Type u} [Semiring R] :
Function.Injective ⇑C
source
@[simp]
theorem Polynomial.C_inj {R : Type u} {a b : R} [Semiring R] :
C a = C b ↔ a = b
source
@[simp]
theorem Polynomial.C_eq_zero {R : Type u} {a : R} [Semiring R] :
C a = 0 ↔ a = 0
source
theorem Polynomial.C_ne_zero {R : Type u} {a : R} [Semiring R] :
C a ≠ 0 ↔ a ≠ 0
source
theorem Polynomial.subsingleton_iff_subsingleton {R : Type u} [Semiring R] :
Subsingleton (Polynomial R) ↔ Subsingleton R
source
theorem Polynomial.Nontrivial.of_polynomial_ne {R : Type u} [Semiring R] {p q : Polynomial R} (h : p ≠ q) :
Nontrivial R
source
theorem Polynomial.forall_eq_iff_forall_eq {R : Type u} [Semiring R] :
(∀ (f g : Polynomial R), f = g) ↔ ∀ (a b : R), a = b
source
theorem Polynomial.ext_iff {R : Type u} [Semiring R] {p q : Polynomial R} :
p = q ↔ ∀ (n : ℕ), p.coeff n = q.coeff n
source
theorem Polynomial.ext {R : Type u} [Semiring R] {p q : Polynomial R} :
(∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
source
theorem Polynomial.addSubmonoid_closure_setOf_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.

source
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
source
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
source
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
source
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
source
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
source
theorem Polynomial.eq_zero_of_eq_zero {R : Type u} [Semiring R] (h : 0 = 1) (p : Polynomial R) :
p = 0
source
theorem Polynomial.support_monomial {R : Type u} [Semiring R] (n : ℕ) {a : R} (H : a ≠ 0) :
((monomial n) a).support = {n}
source
theorem Polynomial.support_monomial' {R : Type u} [Semiring R] (n : ℕ) (a : R) :
((monomial n) a).support ⊆ {n}
source
theorem Polynomial.support_C {R : Type u} [Semiring R] {a : R} (h : a ≠ 0) :
(C a).support = {0}
source
theorem Polynomial.support_C_subset {R : Type u} [Semiring R] (a : R) :
(C a).support ⊆ {0}
source
theorem Polynomial.support_C_mul_X {R : Type u} [Semiring R] {c : R} (h : c ≠ 0) :
(C c * X).support = {1}
source
theorem Polynomial.support_C_mul_X' {R : Type u} [Semiring R] (c : R) :
(C c * X).support ⊆ {1}
source
theorem Polynomial.support_C_mul_X_pow {R : Type u} [Semiring R] (n : ℕ) {c : R} (h : c ≠ 0) :
(C c * X ^ n).support = {n}
source
theorem Polynomial.support_C_mul_X_pow' {R : Type u} [Semiring R] (n : ℕ) (c : R) :
(C c * X ^ n).support ⊆ {n}
source
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}
source
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}
source
theorem Polynomial.X_pow_eq_monomial {R : Type u} [Semiring R] (n : ℕ) :
X ^ n = (monomial n) 1
source
@[simp]
theorem Polynomial.toFinsupp_X_pow {R : Type u} [Semiring R] (n : ℕ) :
(X ^ n).toFinsupp = Finsupp.single n 1
source
theorem Polynomial.smul_X_eq_monomial {R : Type u} {a : R} [Semiring R] {n : ℕ} :
a • X ^ n = (monomial n) a
source
theorem Polynomial.support_X_pow {R : Type u} [Semiring R] (H : ¬1 = 0) (n : ℕ) :
(X ^ n).support = {n}
source
theorem Polynomial.support_X_empty {R : Type u} [Semiring R] (H : 1 = 0) :
X.support = ∅
source
theorem Polynomial.support_X {R : Type u} [Semiring R] (H : ¬1 = 0) :
X.support = {1}
source
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
source
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
source
theorem Polynomial.natCast_mul {R : Type u} [Semiring R] (n : ℕ) (p : Polynomial R) :
↑n * p = n • p
source
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)

Instances For

source
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)
source
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)
source
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.

source
@[simp]
theorem Polynomial.sum_zero_index {R : Type u} [Semiring R] {S : Type u_1} [AddCommMonoid S] (f : ℕ → R → S) :
sum 0 f = 0
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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)
source
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)
source
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
source
@[simp]
theorem Polynomial.sum_monomial_eq {R : Type u} [Semiring R] (p : Polynomial R) :
(p.sum fun (n : ℕ) (a : R) => (monomial n) a) = p
source
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
source
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
source
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.

source
theorem Polynomial.erase_def {R : Type u_1} [Semiring R] (n : ℕ) (x✝ : Polynomial R) :
erase n x✝ = match x✝ with | { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }
source
@[irreducible]
def Polynomial.erase {R : Type u_1} [Semiring R] (n : ℕ) :
Polynomial R → Polynomial R

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

Equations

- Polynomial.erase n x✝ = match x✝ with | { toFinsupp := p } => { toFinsupp := Finsupp.erase n p }

Instances For

source
@[simp]
theorem Polynomial.toFinsupp_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(erase n p).toFinsupp = Finsupp.erase n p.toFinsupp
source
@[simp]
theorem Polynomial.ofFinsupp_erase {R : Type u} [Semiring R] (p : AddMonoidAlgebra R ℕ) (n : ℕ) :
{ toFinsupp := Finsupp.erase n p } = erase n { toFinsupp := p }
source
@[simp]
theorem Polynomial.support_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(erase n p).support = p.support.erase n
source
theorem Polynomial.monomial_add_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(monomial n) (p.coeff n) + erase n p = p
source
theorem Polynomial.coeff_erase {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) :
(erase n p).coeff i = if i = n then 0 else p.coeff i
source
@[simp]
theorem Polynomial.erase_zero {R : Type u} [Semiring R] (n : ℕ) :
erase n 0 = 0
source
@[simp]
theorem Polynomial.erase_monomial {R : Type u} [Semiring R] {n : ℕ} {a : R} :
erase n ((monomial n) a) = 0
source
@[simp]
theorem Polynomial.erase_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(erase n p).coeff n = 0
source
@[simp]
theorem Polynomial.erase_ne {R : Type u} [Semiring R] (p : Polynomial R) (n i : ℕ) (h : i ≠ n) :
(erase n p).coeff i = p.coeff i
source
def Polynomial.update {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) :
Polynomial 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.natDegree < n` and `a ≠ 0`, this increases the degree to `n`.

Equations

- p.update n a = { toFinsupp := Finsupp.update p.toFinsupp n a }

Instances For

source
theorem Polynomial.coeff_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) :
(p.update n a).coeff = Function.update p.coeff n a
source
theorem Polynomial.coeff_update_apply {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) (i : ℕ) :
(p.update n a).coeff i = if i = n then a else p.coeff i
source
@[simp]
theorem Polynomial.coeff_update_same {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) :
(p.update n a).coeff n = a
source
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
source
@[simp]
theorem Polynomial.update_zero_eq_erase {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
p.update n 0 = erase n p
source
theorem Polynomial.support_update {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) (a : R) [Decidable (a = 0)] :
(p.update n a).support = if a = 0 then p.support.erase n else insert n p.support
source
theorem Polynomial.support_update_zero {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) :
(p.update n 0).support = p.support.erase n
source
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 = insert n p.support
source
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

Instances For

source
@[simp]
theorem Polynomial.coeffs_zero {R : Type u} [Semiring R] :
coeffs 0 = ∅
source
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
source
theorem Polynomial.coeffs_one {R : Type u} [Semiring R] :
coeffs 1 ⊆ {1}
source
theorem Polynomial.coeff_mem_coeffs {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : p.coeff n ≠ 0) :
p.coeff n ∈ p.coeffs
source
@[simp]
theorem Polynomial.coeffs_empty_iff {R : Type u} [Semiring R] {p : Polynomial R} :
p.coeffs = ∅ ↔ p = 0
source
@[simp]
theorem Polynomial.coeffs_nonempty_iff {R : Type u} [Semiring R] {p : Polynomial R} :
p.coeffs.Nonempty ↔ p ≠ 0
source
theorem Polynomial.coeffs_monomial {R : Type u} [Semiring R] (n : ℕ) {c : R} (hc : c ≠ 0) :
((monomial n) c).coeffs = {c}
source
instance Polynomial.commSemiring {R : Type u} [CommSemiring R] :
CommSemiring (Polynomial R)
Equations

- Polynomial.commSemiring = { toSemiring := Polynomial.semiring, mul_comm := ⋯ }

source
instance Polynomial.instZSMul {R : Type u} [Ring R] :
SMul ℤ (Polynomial R)
Equations

- Polynomial.instZSMul = { smul := fun (r : ℤ) (p : Polynomial R) => { toFinsupp := r • p.toFinsupp } }

source
@[simp]
theorem Polynomial.ofFinsupp_zsmul {R : Type u} [Ring R] (a : ℤ) (b : AddMonoidAlgebra R ℕ) :
{ toFinsupp := a • b } = a • { toFinsupp := b }
source
@[simp]
theorem Polynomial.toFinsupp_zsmul {R : Type u} [Ring R] (a : ℤ) (b : Polynomial R) :
(a • b).toFinsupp = a • b.toFinsupp
source
instance Polynomial.instIntCast {R : Type u} [Ring R] :
IntCast (Polynomial R)
Equations

- Polynomial.instIntCast = { intCast := fun (n : ℤ) => { toFinsupp := ↑n } }

source
@[simp]
theorem Polynomial.ofFinsupp_intCast {R : Type u} [Ring R] (z : ℤ) :
{ toFinsupp := ↑z } = ↑z
source
@[simp]
theorem Polynomial.toFinsupp_intCast {R : Type u} [Ring R] (z : ℤ) :
(↑z).toFinsupp = ↑z
source
instance Polynomial.ring {R : Type u} [Ring R] :
Ring (Polynomial R)
Equations

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

source
@[simp]
theorem Polynomial.coeff_neg {R : Type u} [Ring R] (p : Polynomial R) (n : ℕ) :
(-p).coeff n = -p.coeff n
source
@[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
source
@[simp]
theorem Polynomial.monomial_neg {R : Type u} [Ring R] (n : ℕ) (a : R) :
(monomial n) (-a) = -(monomial n) a
source
theorem Polynomial.monomial_sub {R : Type u} {a b : R} [Ring R] (n : ℕ) :
(monomial n) (a - b) = (monomial n) a - (monomial n) b
source
@[simp]
theorem Polynomial.support_neg {R : Type u} [Ring R] {p : Polynomial R} :
(-p).support = p.support
source
theorem Polynomial.C_eq_intCast {R : Type u} [Ring R] (n : ℤ) :
C ↑n = ↑n
source
theorem Polynomial.C_neg {R : Type u} {a : R} [Ring R] :
C (-a) = -C a
source
theorem Polynomial.C_sub {R : Type u} {a b : R} [Ring R] :
C (a - b) = C a - C b
source
instance Polynomial.commRing {R : Type u} [CommRing R] :
CommRing (Polynomial R)
Equations

- Polynomial.commRing = { toRing := Polynomial.ring, mul_comm := ⋯ }

source
instance Polynomial.nontrivial {R : Type u} [Semiring R] [Nontrivial R] :
Nontrivial (Polynomial R)
source
@[simp]
theorem Polynomial.X_ne_zero {R : Type u} [Semiring R] [Nontrivial R] :
X ≠ 0
source
instance Polynomial.instNoZeroDivisors {R : Type u} [Semiring R] [NoZeroDivisors R] :
NoZeroDivisors (Polynomial R)
source
instance Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd {R : Type u} [Semiring R] [IsCancelAdd R] [IsLeftCancelMulZero R] :
IsLeftCancelMulZero (Polynomial R)
source
instance Polynomial.instIsRightCancelMulZeroOfIsCancelAdd {R : Type u} [Semiring R] [IsCancelAdd R] [IsRightCancelMulZero R] :
IsRightCancelMulZero (Polynomial R)
source
instance Polynomial.instIsCancelMulZeroOfIsCancelAdd {R : Type u} [Semiring R] [IsCancelAdd R] [IsCancelMulZero R] :
IsCancelMulZero (Polynomial R)
source
instance Polynomial.instIsDomainOfIsCancelAdd {R : Type u} [Semiring R] [IsCancelAdd R] [IsDomain R] :
IsDomain (Polynomial R)
source
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.

source
theorem Polynomial.nnqsmul_eq_C_mul {R : Type u} [DivisionSemiring R] (q : ℚ≥0) (f : Polynomial R) :
q • f = C ↑q * f
source
theorem Polynomial.qsmul_eq_C_mul {R : Type u} [DivisionRing R] (a : ℚ) (f : Polynomial R) :
a • f = C ↑a * f
source
@[simp]
theorem Polynomial.nontrivial_iff {R : Type u} [Semiring R] :
Nontrivial (Polynomial R) ↔ Nontrivial R
source
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.