Theory of univariate polynomials

We show that A[X] is an R-algebra when A is an R-algebra. We promote eval₂ to an algebra hom in aeval.

instance Polynomial.algebraOfAlgebra {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (Polynomial A)

Note that this instance also provides Algebra R R[X].

Equations

• Polynomial.algebraOfAlgebra = { toSMul := Polynomial.smulZeroClass.toSMul, algebraMap := Polynomial.C.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }

@[simp]

theorem Polynomial.algebraMap_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : (algebraMap R (Polynomial A)) r = C ((algebraMap R A) r)

@[simp]

theorem Polynomial.toFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : ((algebraMap R (Polynomial A)) r).toFinsupp = (algebraMap R (AddMonoidAlgebra A ℕ)) r

theorem Polynomial.ofFinsupp_algebraMap {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (r : R) : { toFinsupp := (algebraMap R (AddMonoidAlgebra A ℕ)) r } = (algebraMap R (Polynomial A)) r

theorem Polynomial.C_eq_algebraMap {R : Type u} [CommSemiring R] (r : R) : C r = (algebraMap R (Polynomial R)) r

When we have [CommSemiring R], the function C is the same as algebraMap R R[X].

(But note that C is defined when R is not necessarily commutative, in which case algebraMap is not available.)

@[simp]

theorem Polynomial.algebraMap_eq {R : Type u} [CommSemiring R] : algebraMap R (Polynomial R) = C

def Polynomial.CAlgHom {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] : A →ₐ[R] Polynomial A

Polynomial.C as an AlgHom.

Equations

• Polynomial.CAlgHom = { toRingHom := Polynomial.C, commutes' := ⋯ }

@[simp]

theorem Polynomial.CAlgHom_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : A) : CAlgHom a✝ = C a✝

theorem Polynomial.algHom_ext' {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f g : Polynomial A →ₐ[R] B} (hC : f.comp CAlgHom = g.comp CAlgHom) (hX : f X = g X) : f = g

Extensionality lemma for algebra maps out of A'[X] over a smaller base ring than A'

theorem Polynomial.algHom_ext'_iff {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {f g : Polynomial A →ₐ[R] B} : f = g ↔ f.comp CAlgHom = g.comp CAlgHom ∧ f X = g X

def Polynomial.toFinsuppIsoAlg (R : Type u) [CommSemiring R] : Polynomial R ≃ₐ[R] AddMonoidAlgebra R ℕ

Algebra 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.toFinsuppIsoAlg R = { toEquiv := (Polynomial.toFinsuppIso R).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Polynomial.toFinsuppIsoAlg_apply (R : Type u) [CommSemiring R] (self : Polynomial R) : (toFinsuppIsoAlg R) self = self.toFinsupp

@[simp]

theorem Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp (R : Type u) [CommSemiring R] (toFinsupp : AddMonoidAlgebra R ℕ) : ((toFinsuppIsoAlg R).symm toFinsupp).toFinsupp = toFinsupp

instance Polynomial.subalgebraNontrivial {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] [Nontrivial A] : Nontrivial (Subalgebra R (Polynomial A))

@[simp]

theorem Polynomial.algHom_eval₂_algebraMap {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (p : Polynomial R) (f : A →ₐ[R] B) (a : A) : f (eval₂ (algebraMap R A) a p) = eval₂ (algebraMap R B) (f a) p

@[simp]

theorem Polynomial.eval₂_algebraMap_X {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) (f : Polynomial R →ₐ[R] A) : eval₂ (algebraMap R A) (f X) p = f p

@[simp]

theorem Polynomial.ringHom_eval₂_intCastRingHom {R : Type u_3} {S : Type u_4} [Ring R] [Ring S] (p : Polynomial ℤ) (f : R →+* S) (r : R) : f (eval₂ (Int.castRingHom R) r p) = eval₂ (Int.castRingHom S) (f r) p

@[simp]

theorem Polynomial.eval₂_intCastRingHom_X {R : Type u_3} [Ring R] (p : Polynomial ℤ) (f : Polynomial ℤ →+* R) : eval₂ (Int.castRingHom R) (f X) p = f p

def Polynomial.eval₂AlgHom' {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) : Polynomial A →ₐ[R] B

Polynomial.eval₂ as an AlgHom for noncommutative algebras.

This is Polynomial.eval₂RingHom' for AlgHoms.

Equations

• Polynomial.eval₂AlgHom' f b hf = { toRingHom := Polynomial.eval₂RingHom' (↑f) b hf, commutes' := ⋯ }

@[simp]

theorem Polynomial.eval₂AlgHom'_apply {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (b : B) (hf : ∀ (a : A), Commute (f a) b) (p : Polynomial A) : (eval₂AlgHom' f b hf) p = eval₂ (↑f) b p

def Polynomial.mapAlgHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : Polynomial A →ₐ[R] Polynomial B

Polynomial.map as an AlgHom for noncommutative algebras.

This is the algebra version of Polynomial.mapRingHom.

Equations

• Polynomial.mapAlgHom f = { toRingHom := Polynomial.mapRingHom f.toRingHom, commutes' := ⋯ }

@[simp]

theorem Polynomial.coe_mapAlgHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : ⇑(mapAlgHom f) = map ↑f

@[simp]

theorem Polynomial.mapAlgHom_id {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] : mapAlgHom (AlgHom.id R A) = AlgHom.id R (Polynomial A)

@[simp]

theorem Polynomial.mapAlgHom_coe_ringHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : ↑(mapAlgHom f) = mapRingHom ↑f

@[simp]

theorem Polynomial.mapAlgHom_comp {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (C : Type u_3) [Semiring C] [Algebra R C] (f : B →ₐ[R] C) (g : A →ₐ[R] B) : (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

theorem Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : mapAlgHom f = eval₂AlgHom' (CAlgHom.comp f) X ⋯

def Polynomial.mapAlgEquiv {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : Polynomial A ≃ₐ[R] Polynomial B

If A and B are isomorphic as R-algebras, then so are their polynomial rings

Equations

• Polynomial.mapAlgEquiv f = AlgEquiv.ofAlgHom (Polynomial.mapAlgHom ↑f) (Polynomial.mapAlgHom ↑f.symm) ⋯ ⋯

@[simp]

theorem Polynomial.coe_mapAlgEquiv {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : ⇑(mapAlgEquiv f) = map ↑f

@[simp]

theorem Polynomial.mapAlgEquiv_id {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] : mapAlgEquiv AlgEquiv.refl = AlgEquiv.refl

@[simp]

theorem Polynomial.mapAlgEquiv_coe_ringHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : ↑(mapAlgEquiv f) = mapRingHom ↑f

@[simp]

theorem Polynomial.mapAlgEquiv_toAlgHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : ↑(mapAlgEquiv f) = mapAlgHom ↑f

@[simp]

theorem Polynomial.mapAlgEquiv_comp {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (C : Type u_3) [Semiring C] [Algebra R C] (f : A ≃ₐ[R] B) (g : B ≃ₐ[R] C) : (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

def Polynomial.aeval {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : Polynomial R →ₐ[R] A

Given a valuation x of the variable in an R-algebra A, aeval R A x is the unique R-algebra homomorphism from R[X] to A sending X to x.

This is a stronger variant of the linear map Polynomial.leval.

Equations

• Polynomial.aeval x = Polynomial.eval₂AlgHom' (Algebra.ofId R A) x ⋯

def Polynomial.mapAlg (R : Type u) [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] : Polynomial R →ₐ[R] Polynomial S

The map R[X] → S[X] as an algebra homomorphism.

Equations

• Polynomial.mapAlg R S = Polynomial.aeval Polynomial.X

theorem Polynomial.algHom_ext {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {f g : Polynomial R →ₐ[R] B} (hX : f X = g X) : f = g

theorem Polynomial.algHom_ext_iff {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] {f g : Polynomial R →ₐ[R] B} : f = g ↔ f X = g X

theorem Polynomial.aeval_def {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (p : Polynomial R) : (aeval x) p = eval₂ (algebraMap R A) x p

@[simp]

theorem Polynomial.eval_map_algebraMap {R : Type u} {B : Type u_2} [CommSemiring R] [Semiring B] [Algebra R B] (P : Polynomial R) (b : B) : eval b (map (algebraMap R B) P) = (aeval b) P

theorem Polynomial.mapAlg_eq_map {R : Type u} [CommSemiring R] (S : Type v) [Semiring S] [Algebra R S] (p : Polynomial R) : (mapAlg R S) p = map (algebraMap R S) p

mapAlg is the morphism induced by R → S.

theorem Polynomial.aeval_zero {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (aeval x) 0 = 0

@[simp]

theorem Polynomial.aeval_X {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (aeval x) X = x

@[simp]

theorem Polynomial.aeval_C {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (r : R) : (aeval x) (C r) = (algebraMap R A) r

@[simp]

theorem Polynomial.aeval_monomial {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} {r : R} : (aeval x) ((monomial n) r) = (algebraMap R A) r * x ^ n

theorem Polynomial.aeval_X_pow {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {n : ℕ} : (aeval x) (X ^ n) = x ^ n

theorem Polynomial.aeval_add {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial R} (x : A) : (aeval x) (p + q) = (aeval x) p + (aeval x) q

theorem Polynomial.aeval_one {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : (aeval x) 1 = 1

theorem Polynomial.aeval_natCast {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (n : ℕ) : (aeval x) ↑n = ↑n

theorem Polynomial.aeval_mul {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p q : Polynomial R} (x : A) : (aeval x) (p * q) = (aeval x) p * (aeval x) q

theorem Polynomial.comp_eq_aeval {R : Type u} [CommSemiring R] {p q : Polynomial R} : p.comp q = (aeval q) p

theorem Polynomial.aeval_comp {R : Type u} [CommSemiring R] {p q : Polynomial R} {A : Type u_3} [Semiring A] [Algebra R A] (x : A) : (aeval x) (p.comp q) = (aeval ((aeval x) q)) p

theorem Polynomial.mapAlg_comp {A : Type u_3} (B : Type u_4) (C : Type u_5) [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] (p : Polynomial A) : (mapAlg A C) p = (mapAlg B C) ((mapAlg A B) p)

theorem Polynomial.coeff_zero_of_isScalarTower {A : Type u_3} (B : Type u_4) (C : Type u_5) [CommSemiring A] [CommSemiring B] [Semiring C] [Algebra A B] [Algebra A C] [Algebra B C] [IsScalarTower A B C] (p : Polynomial A) : (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = ((mapAlg A C) p).coeff 0

def Polynomial.algEquivOfCompEqX {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = X) (hqp : q.comp p = X) : Polynomial R ≃ₐ[R] Polynomial R

Two polynomials p and q such that p(q(X))=X and q(p(X))=X induces an automorphism of the polynomial algebra.

Equations

• p.algEquivOfCompEqX q hpq hqp = AlgEquiv.ofAlgHom (Polynomial.aeval p) (Polynomial.aeval q) ⋯ ⋯

@[simp]

theorem Polynomial.algEquivOfCompEqX_apply {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = X) (hqp : q.comp p = X) (a : Polynomial R) : (p.algEquivOfCompEqX q hpq hqp) a = (aeval p) a

@[simp]

theorem Polynomial.algEquivOfCompEqX_symm_apply {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = X) (hqp : q.comp p = X) (a : Polynomial R) : (p.algEquivOfCompEqX q hpq hqp).symm a = (aeval q) a

@[simp]

theorem Polynomial.algEquivOfCompEqX_eq_iff {R : Type u} [CommSemiring R] (p q p' q' : Polynomial R) (hpq : p.comp q = X) (hqp : q.comp p = X) (hpq' : p'.comp q' = X) (hqp' : q'.comp p' = X) : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp' ↔ p = p'

@[simp]

theorem Polynomial.algEquivOfCompEqX_symm {R : Type u} [CommSemiring R] (p q : Polynomial R) (hpq : p.comp q = X) (hqp : q.comp p = X) : (p.algEquivOfCompEqX q hpq hqp).symm = q.algEquivOfCompEqX p hqp hpq

def Polynomial.algEquivCMulXAddC {R : Type u_3} [CommRing R] (a b : R) [Invertible a] : Polynomial R ≃ₐ[R] Polynomial R

The automorphism of the polynomial algebra given by p(X) ↦ p(a * X + b), with inverse p(X) ↦ p(a⁻¹ * (X - b)).

Equations

• Polynomial.algEquivCMulXAddC a b = (Polynomial.C a * Polynomial.X + Polynomial.C b).algEquivOfCompEqX (Polynomial.C ⅟a * (Polynomial.X - Polynomial.C b)) ⋯ ⋯

@[simp]

theorem Polynomial.algEquivCMulXAddC_symm_apply {R : Type u_3} [CommRing R] (a b : R) [Invertible a] (a✝ : Polynomial R) : (algEquivCMulXAddC a b).symm a✝ = (aeval (C ⅟a * (X - C b))) a✝

@[simp]

theorem Polynomial.algEquivCMulXAddC_apply {R : Type u_3} [CommRing R] (a b : R) [Invertible a] (a✝ : Polynomial R) : (algEquivCMulXAddC a b) a✝ = (aeval (C a * X + C b)) a✝

theorem Polynomial.algEquivCMulXAddC_symm_eq {R : Type u_3} [CommRing R] (a b : R) [Invertible a] : (algEquivCMulXAddC a b).symm = algEquivCMulXAddC (⅟a) (-⅟a * b)

def Polynomial.algEquivAevalXAddC {R : Type u_3} [CommRing R] (t : R) : Polynomial R ≃ₐ[R] Polynomial R

The automorphism of the polynomial algebra given by p(X) ↦ p(X+t), with inverse p(X) ↦ p(X-t).

Equations

• Polynomial.algEquivAevalXAddC t = (Polynomial.X + Polynomial.C t).algEquivOfCompEqX (Polynomial.X - Polynomial.C t) ⋯ ⋯

@[simp]

theorem Polynomial.algEquivAevalXAddC_apply {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) : (algEquivAevalXAddC t) a = (aeval (X + C t)) a

@[simp]

theorem Polynomial.algEquivAevalXAddC_symm_apply {R : Type u_3} [CommRing R] (t : R) (a : Polynomial R) : (algEquivAevalXAddC t).symm a = (aeval (X - C t)) a

@[simp]

theorem Polynomial.algEquivAevalXAddC_eq_iff {R : Type u_3} [CommRing R] (t t' : R) : algEquivAevalXAddC t = algEquivAevalXAddC t' ↔ t = t'

@[simp]

theorem Polynomial.algEquivAevalXAddC_symm {R : Type u_3} [CommRing R] (t : R) : (algEquivAevalXAddC t).symm = algEquivAevalXAddC (-t)

def Polynomial.algEquivAevalNegX {R : Type u_3} [CommRing R] : Polynomial R ≃ₐ[R] Polynomial R

The involutive automorphism of the polynomial algebra given by p(X) ↦ p(-X).

Equations

• Polynomial.algEquivAevalNegX = (-Polynomial.X).algEquivOfCompEqX (-Polynomial.X) ⋯ ⋯

@[simp]

theorem Polynomial.algEquivAevalNegX_apply {R : Type u_3} [CommRing R] (a : Polynomial R) : algEquivAevalNegX a = (aeval (-X)) a

@[simp]

theorem Polynomial.algEquivAevalNegX_symm_apply {R : Type u_3} [CommRing R] (a : Polynomial R) : algEquivAevalNegX.symm a = (aeval (-X)) a

theorem Polynomial.comp_neg_X_comp_neg_X {R : Type u_3} [CommRing R] (p : Polynomial R) : (p.comp (-X)).comp (-X) = p

theorem Polynomial.aeval_algHom {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (x : A) : aeval (f x) = f.comp (aeval x)

@[simp]

theorem Polynomial.aeval_X_left {R : Type u} [CommSemiring R] : aeval X = AlgHom.id R (Polynomial R)

theorem Polynomial.aeval_X_left_apply {R : Type u} [CommSemiring R] (p : Polynomial R) : (aeval X) p = p

theorem Polynomial.eval_unique {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (φ : Polynomial R →ₐ[R] A) (p : Polynomial R) : φ p = eval₂ (algebraMap R A) (φ X) p

theorem Polynomial.aeval_algHom_apply {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] {F : Type u_3} [FunLike F A B] [AlgHomClass F R A B] (f : F) (x : A) (p : Polynomial R) : (aeval (f x)) p = f ((aeval x) p)

@[simp]

theorem Polynomial.coe_aeval_mk_apply {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) {S : Subalgebra R A} (h : x ∈ S) : ↑((aeval ⟨x, h⟩) p) = (aeval x) p

theorem Polynomial.aeval_algEquiv {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (↑f).comp (aeval x)

theorem Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : R) (p : Polynomial R) : (aeval ((algebraMap R A) x)) p = (algebraMap R A) (eval x p)

theorem Polynomial.aeval_prod {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A × B) : aeval x = (aeval x.1).prod (aeval x.2)

Polynomial evaluation on a pair is a product of the evaluations on the components.

theorem Polynomial.aeval_prod_apply {R : Type u} {A : Type z} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (x : A × B) (p : Polynomial R) : (aeval x) p = ((aeval x.1) p, (aeval x.2) p)

Polynomial evaluation on a pair is a pair of evaluations.

theorem Polynomial.aeval_pi {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) : aeval x = Pi.algHom R A fun (i : I) => aeval (x i)

Polynomial evaluation on an indexed tuple is the indexed product of the evaluations on the components. Generalizes Polynomial.aeval_prod to indexed products.

theorem Polynomial.aeval_pi_apply₂ {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R) (j : I) : (aeval x) p j = (aeval (x j)) p

theorem Polynomial.aeval_pi_apply {R : Type u} [CommSemiring R] {I : Type u_3} {A : I → Type u_4} [(i : I) → Semiring (A i)] [(i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R) : (aeval x) p = fun (j : I) => (aeval (x j)) p

Polynomial evaluation on an indexed tuple is the indexed tuple of the evaluations on the components. Generalizes Polynomial.aeval_prod_apply to indexed products.

@[simp]

theorem Polynomial.coe_aeval_eq_eval {R : Type u} [CommSemiring R] (r : R) : ⇑(aeval r) = eval r

@[simp]

theorem Polynomial.coe_aeval_eq_evalRingHom {R : Type u} [CommSemiring R] (x : R) : ↑(aeval x) = evalRingHom x

@[simp]

theorem Polynomial.aeval_fn_apply {R : Type u} [CommSemiring R] {X : Type u_3} (g : Polynomial R) (f : X → R) (x : X) : (aeval f) g x = (aeval (f x)) g

theorem Polynomial.aeval_subalgebra_coe {R : Type u} [CommSemiring R] (g : Polynomial R) {A : Type u_3} [Semiring A] [Algebra R A] (s : Subalgebra R A) (f : ↥s) : ↑((aeval f) g) = (aeval ↑f) g

theorem Polynomial.coeff_zero_eq_aeval_zero {R : Type u} [CommSemiring R] (p : Polynomial R) : p.coeff 0 = (aeval 0) p

theorem Polynomial.coeff_zero_eq_aeval_zero' {R : Type u} {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (p : Polynomial R) : (algebraMap R A) (p.coeff 0) = (aeval 0) p

theorem Polynomial.map_aeval_eq_aeval_map {R : Type u} [CommSemiring R] {S : Type u_3} {T : Type u_4} {U : Type u_5} [Semiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U] {φ : R →+* T} {ψ : S →+* U} (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : Polynomial R) (a : S) : ψ ((aeval a) p) = (aeval (ψ a)) (map φ p)

theorem Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero {S : Type v} {T : Type w} [CommSemiring S] [CommSemiring T] [Algebra S T] {p q : Polynomial S} (h₁ : p ∣ q) {a : T} (h₂ : (aeval a) p = 0) : (aeval a) q = 0

theorem Polynomial.aeval_eq_sum_range {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (x : S) : (aeval x) p = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i • x ^ i

theorem Polynomial.aeval_eq_sum_range' {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) (x : S) : (aeval x) p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i

theorem Polynomial.isRoot_of_eval₂_map_eq_zero {R : Type u} {S : Type v} [CommSemiring R] {p : Polynomial R} [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {r : R} : eval₂ f (f r) p = 0 → p.IsRoot r

theorem Polynomial.isRoot_of_aeval_algebraMap_eq_zero {R : Type u} {S : Type v} [CommSemiring R] [Semiring S] [Algebra R S] {p : Polynomial R} (inj : Function.Injective ⇑(algebraMap R S)) {r : R} (hr : (aeval ((algebraMap R S) r)) p = 0) : p.IsRoot r

def Polynomial.aevalTower {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (f : R →ₐ[S] A') (x : A') : Polynomial R →ₐ[S] A'

Version of aeval for defining algebra homs out of R[X] over a smaller base ring than R.

Equations

• Polynomial.aevalTower f x = Polynomial.eval₂AlgHom' f x ⋯

@[simp]

theorem Polynomial.aevalTower_X {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') : (aevalTower g y) X = y

@[simp]

theorem Polynomial.aevalTower_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) : (aevalTower g y) (C x) = g x

@[simp]

theorem Polynomial.aevalTower_comp_C {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') : (↑(aevalTower g y)).comp C = ↑g

theorem Polynomial.aevalTower_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) : (aevalTower g y) ((algebraMap R (Polynomial R)) x) = g x

theorem Polynomial.aevalTower_comp_algebraMap {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') : (↑(aevalTower g y)).comp (algebraMap R (Polynomial R)) = ↑g

theorem Polynomial.aevalTower_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') (x : R) : (aevalTower g y) ((IsScalarTower.toAlgHom S R (Polynomial R)) x) = g x

@[simp]

theorem Polynomial.aevalTower_comp_toAlgHom {R : Type u} {S : Type v} {A' : Type u_1} [CommSemiring R] [CommSemiring A'] [CommSemiring S] [Algebra S R] [Algebra S A'] (g : R →ₐ[S] A') (y : A') : (aevalTower g y).comp (IsScalarTower.toAlgHom S R (Polynomial R)) = g

@[simp]

theorem Polynomial.aevalTower_id {S : Type v} [CommSemiring S] : aevalTower (AlgHom.id S S) = aeval

@[simp]

theorem Polynomial.aevalTower_ofId {S : Type v} {A' : Type u_1} [CommSemiring A'] [CommSemiring S] [Algebra S A'] : aevalTower (Algebra.ofId S A') = aeval

theorem Polynomial.dvd_term_of_dvd_eval_of_dvd_terms {S : Type v} [CommRing S] {z p : S} {f : Polynomial S} (i : ℕ) (dvd_eval : p ∣ eval z f) (dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j) : p ∣ f.coeff i * z ^ i

theorem Polynomial.dvd_term_of_isRoot_of_dvd_terms {S : Type v} [CommRing S] {r p : S} {f : Polynomial S} (i : ℕ) (hr : f.IsRoot r) (h : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j) : p ∣ f.coeff i * r ^ i

theorem Polynomial.eval_mul_X_sub_C {R : Type u} [Ring R] {p : Polynomial R} (r : R) : eval r (p * (X - C r)) = 0

The evaluation map is not generally multiplicative when the coefficient ring is noncommutative, but nevertheless any polynomial of the form p * (X - monomial 0 r) is sent to zero when evaluated at r.

This is the key step in our proof of the Cayley-Hamilton theorem.

theorem Polynomial.not_isUnit_X_sub_C {R : Type u} [Ring R] [Nontrivial R] (r : R) : ¬IsUnit (X - C r)

@[simp]

theorem Polynomial.aeval_neg {R : Type u} {A : Type z} [CommRing R] {p : Polynomial R} [Ring A] [Algebra R A] (x : A) : (aeval x) (-p) = -(aeval x) p

@[simp]

theorem Polynomial.aeval_sub {R : Type u} {A : Type z} [CommRing R] {p q : Polynomial R} [Ring A] [Algebra R A] (x : A) : (aeval x) (p - q) = (aeval x) p - (aeval x) q

theorem Polynomial.aeval_endomorphism {R : Type u} [CommRing R] {M : Type u_3} [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) (p : Polynomial R) : ((aeval f) p) v = p.sum fun (n : ℕ) (b : R) => b • (f ^ n) v

theorem Polynomial.X_sub_C_pow_dvd_iff {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} : (X - C t) ^ n ∣ p ↔ X ^ n ∣ p.comp (X + C t)

theorem Polynomial.comp_X_add_C_eq_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : p.comp (X + C t) = 0 ↔ p = 0

theorem Polynomial.comp_X_add_C_ne_zero_iff {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : p.comp (X + C t) ≠ 0 ↔ p ≠ 0

theorem Polynomial.dvd_comp_C_mul_X_add_C_iff {R : Type u} [CommRing R] (p q : Polynomial R) (a b : R) [Invertible a] : p ∣ q.comp (C a * X + C b) ↔ p.comp (C ⅟a * (X - C b)) ∣ q

theorem Polynomial.dvd_comp_X_sub_C_iff {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q

theorem Polynomial.dvd_comp_X_add_C_iff {R : Type u} [CommRing R] (p q : Polynomial R) (a : R) : p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q

theorem Polynomial.dvd_comp_neg_X_iff {R : Type u} [CommRing R] (p q : Polynomial R) : p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

theorem Polynomial.units_coeff_zero_smul {R : Type u} [CommRing R] [IsDomain R] (c : (Polynomial R)ˣ) (p : Polynomial R) : (↑c).coeff 0 • p = ↑c * p

theorem Polynomial.aeval_apply_smul_mem_of_le_comap' {R : Type u} {A : Type z} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} [Semiring A] [Algebra R A] [Module A M] [IsScalarTower R A M] (hm : m ∈ q) (p : Polynomial R) (a : A) (hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a) q) : (aeval a) p • m ∈ q

theorem Polynomial.aeval_apply_smul_mem_of_le_comap {R : Type u} {M : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] {q : Submodule R M} {m : M} (hm : m ∈ q) (p : Polynomial R) (f : Module.End R M) (hq : q ≤ Submodule.comap f q) : ((aeval f) p) m ∈ q

@[irreducible]

theorem Polynomial.eq_zero_of_mul_eq_zero_of_smul {R : Type u} [CommSemiring R] (P : Polynomial R) (h : ∀ (r : R), r • P = 0 → r = 0) (Q : Polynomial R) (hQ : P * Q = 0) : Q = 0

theorem Polynomial.notMem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} : P ∉ nonZeroDivisors (Polynomial R) ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0

McCoy theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

@[deprecated Polynomial.notMem_nonZeroDivisors_iff (since := "2025-05-24")]

theorem Polynomial.nmem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} : P ∉ nonZeroDivisors (Polynomial R) ↔ ∃ (a : R), a ≠ 0 ∧ a • P = 0

Alias of Polynomial.notMem_nonZeroDivisors_iff.

---

McCoy theorem: a polynomial P : R[X] is a zerodivisor if and only if there is a : R such that a ≠ 0 and a • P = 0.

theorem Polynomial.mem_nonZeroDivisors_iff {R : Type u} [CommSemiring R] {P : Polynomial R} : P ∈ nonZeroDivisors (Polynomial R) ↔ ∀ (a : R), a • P = 0 → a = 0

theorem Polynomial.mem_nonzeroDivisors_of_coeff_mem {R : Type u} [CommSemiring R] {p : Polynomial R} (n : ℕ) (hp : p.coeff n ∈ nonZeroDivisors R) : p ∈ nonZeroDivisors (Polynomial R)

theorem Polynomial.X_mem_nonzeroDivisors {R : Type u} [CommSemiring R] : X ∈ nonZeroDivisors (Polynomial R)