Ring-theoretic supplement of Data.Polynomial.

Main results

• MvPolynomial.isDomain: If a ring is an integral domain, then so is its polynomial ring over finitely many variables.
• Polynomial.isNoetherianRing: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
• Polynomial.wfDvdMonoid: If an integral domain is a WFDvdMonoid, then so is its polynomial ring.
• Polynomial.uniqueFactorizationMonoid, MvPolynomial.uniqueFactorizationMonoid: If an integral domain is a UniqueFactorizationMonoid, then so is its polynomial ring (of any number of variables).

instance Polynomial.instCharP {R : Type u} [Semiring R] (p : ℕ) [h : CharP R p] : CharP (Polynomial R) p

Equations

• ⋯ = ⋯

instance Polynomial.instExpChar {R : Type u} [Semiring R] (p : ℕ) [h : ExpChar R p] : ExpChar (Polynomial R) p

Equations

• ⋯ = ⋯

def Polynomial.degreeLE (R : Type u) [Semiring R] (n : WithBot ℕ) : Submodule R (Polynomial R)

The R-submodule of R[X] consisting of polynomials of degree ≤ n.

Equations

• Polynomial.degreeLE R n = ⨅ (k : ℕ), ⨅ (_ : ↑k > n), LinearMap.ker (Polynomial.lcoeff R k)

def Polynomial.degreeLT (R : Type u) [Semiring R] (n : ℕ) : Submodule R (Polynomial R)

The R-submodule of R[X] consisting of polynomials of degree < n.

Equations

• Polynomial.degreeLT R n = ⨅ (k : ℕ), ⨅ (_ : k ≥ n), LinearMap.ker (Polynomial.lcoeff R k)

theorem Polynomial.mem_degreeLE {R : Type u} [Semiring R] {n : WithBot ℕ} {f : Polynomial R} : f ∈ Polynomial.degreeLE R n ↔ Polynomial.degree f ≤ n

theorem Polynomial.degreeLE_mono {R : Type u} [Semiring R] {m : WithBot ℕ} {n : WithBot ℕ} (H : m ≤ n) : Polynomial.degreeLE R m ≤ Polynomial.degreeLE R n

theorem Polynomial.degreeLE_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : ℕ} : Polynomial.degreeLE R ↑n = Submodule.span R ↑(Finset.image (fun (n : ℕ) => Polynomial.X ^ n) (Finset.range (n + 1)))

theorem Polynomial.mem_degreeLT {R : Type u} [Semiring R] {n : ℕ} {f : Polynomial R} : f ∈ Polynomial.degreeLT R n ↔ Polynomial.degree f < ↑n

theorem Polynomial.degreeLT_mono {R : Type u} [Semiring R] {m : ℕ} {n : ℕ} (H : m ≤ n) : Polynomial.degreeLT R m ≤ Polynomial.degreeLT R n

theorem Polynomial.degreeLT_eq_span_X_pow {R : Type u} [Semiring R] [DecidableEq R] {n : ℕ} : Polynomial.degreeLT R n = Submodule.span R ↑(Finset.image (fun (n : ℕ) => Polynomial.X ^ n) (Finset.range n))

def Polynomial.degreeLTEquiv (R : Type u_2) [Semiring R] (n : ℕ) : ↥(Polynomial.degreeLT R n) ≃ₗ[R] Fin n → R

The first n coefficients on degreeLT n form a linear equivalence with Fin n → R.

Equations

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

theorem Polynomial.degreeLTEquiv_eq_zero_iff_eq_zero {R : Type u} [Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ Polynomial.degreeLT R n) : (Polynomial.degreeLTEquiv R n) { val := p, property := hp } = 0 ↔ p = 0

theorem Polynomial.eval_eq_sum_degreeLTEquiv {R : Type u} [Semiring R] {n : ℕ} {p : Polynomial R} (hp : p ∈ Polynomial.degreeLT R n) (x : R) : Polynomial.eval x p = Finset.sum Finset.univ fun (i : Fin n) => (Polynomial.degreeLTEquiv R n) { val := p, property := hp } i * x ^ ↑i

theorem Polynomial.degreeLT_succ_eq_degreeLE {R : Type u} [Semiring R] {n : ℕ} : Polynomial.degreeLT R (n + 1) = Polynomial.degreeLE R ↑n

theorem Polynomial.exists_degree_le_of_mem_span {R : Type u} [Semiring R] {s : Set (Polynomial R)} {p : Polynomial R} (hs : Set.Nonempty s) (hp : p ∈ Submodule.span R s) : ∃ p' ∈ s, Polynomial.degree p ≤ Polynomial.degree p'

For every polynomial p in the span of a set s : Set R[X], there exists a polynomial of p' ∈ s with higher degree. See also Polynomial.exists_degree_le_of_mem_span_of_finite.

theorem Polynomial.exists_degree_le_of_mem_span_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : Set.Finite s) (hs : Set.Nonempty s) : ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, Polynomial.degree p ≤ Polynomial.degree p'

A stronger version of Polynomial.exists_degree_le_of_mem_span under the assumption that the set s : R[X] is finite. There exists a polynomial p' ∈ s whose degree dominates the degree of every element of p ∈ span R s

theorem Polynomial.span_le_degreeLE_of_finite {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : Set.Finite s) : ∃ (n : ℕ), Submodule.span R s ≤ Polynomial.degreeLE R ↑n

The span of every finite set of polynomials is contained in a degreeLE n for some n.

theorem Polynomial.span_of_finite_le_degreeLT {R : Type u} [Semiring R] {s : Set (Polynomial R)} (s_fin : Set.Finite s) : ∃ (n : ℕ), Submodule.span R s ≤ Polynomial.degreeLT R n

The span of every finite set of polynomials is contained in a degreeLT n for some n.

theorem Polynomial.not_finite {R : Type u} [Semiring R] [Nontrivial R] : ¬Module.Finite R (Polynomial R)

If R is a nontrivial ring, the polynomials R[X] are not finite as an R-module. When R is a field, this is equivalent to R[X] being an infinite-dimensional vector space over R.

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

The finset of nonzero coefficients of a polynomial.

Equations

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

theorem Polynomial.frange_zero {R : Type u} [Semiring R] : Polynomial.frange 0 = ∅

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

theorem Polynomial.frange_one {R : Type u} [Semiring R] : Polynomial.frange 1 ⊆ {1}

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

theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [Semiring R] (n : ℕ) : Polynomial.comp (Finset.sum (Finset.range n) fun (i : ℕ) => Polynomial.X ^ i) (Polynomial.X + 1) = Finset.sum (Finset.range n) fun (i : ℕ) => ↑(Nat.choose n (i + 1)) * Polynomial.X ^ i

theorem Polynomial.Monic.geom_sum {R : Type u} [Semiring R] {P : Polynomial R} (hP : Polynomial.Monic P) (hdeg : 0 < Polynomial.natDegree P) {n : ℕ} (hn : n ≠ 0) : Polynomial.Monic (Finset.sum (Finset.range n) fun (i : ℕ) => P ^ i)

theorem Polynomial.Monic.geom_sum' {R : Type u} [Semiring R] {P : Polynomial R} (hP : Polynomial.Monic P) (hdeg : 0 < Polynomial.degree P) {n : ℕ} (hn : n ≠ 0) : Polynomial.Monic (Finset.sum (Finset.range n) fun (i : ℕ) => P ^ i)

theorem Polynomial.monic_geom_sum_X {R : Type u} [Semiring R] {n : ℕ} (hn : n ≠ 0) : Polynomial.Monic (Finset.sum (Finset.range n) fun (i : ℕ) => Polynomial.X ^ i)

def Polynomial.restriction {R : Type u} [Ring R] (p : Polynomial R) : Polynomial ↥(Subring.closure ↑(Polynomial.frange p))

Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.

Equations

• Polynomial.restriction p = Finset.sum (Polynomial.support p) fun (i : ℕ) => (Polynomial.monomial i) { val := Polynomial.coeff p i, property := ⋯ }

@[simp]

theorem Polynomial.coeff_restriction {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} : ↑(Polynomial.coeff (Polynomial.restriction p) n) = Polynomial.coeff p n

theorem Polynomial.coeff_restriction' {R : Type u} [Ring R] {p : Polynomial R} {n : ℕ} : ↑(Polynomial.coeff (Polynomial.restriction p) n) = Polynomial.coeff p n

@[simp]

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

@[simp]

theorem Polynomial.map_restriction {R : Type u} [CommRing R] (p : Polynomial R) : Polynomial.map (algebraMap (↥(Subring.closure ↑(Polynomial.frange p))) R) (Polynomial.restriction p) = p

@[simp]

theorem Polynomial.degree_restriction {R : Type u} [Ring R] {p : Polynomial R} : Polynomial.degree (Polynomial.restriction p) = Polynomial.degree p

@[simp]

theorem Polynomial.natDegree_restriction {R : Type u} [Ring R] {p : Polynomial R} : Polynomial.natDegree (Polynomial.restriction p) = Polynomial.natDegree p

@[simp]

theorem Polynomial.monic_restriction {R : Type u} [Ring R] {p : Polynomial R} : Polynomial.Monic (Polynomial.restriction p) ↔ Polynomial.Monic p

@[simp]

theorem Polynomial.restriction_zero {R : Type u} [Ring R] : Polynomial.restriction 0 = 0

@[simp]

theorem Polynomial.restriction_one {R : Type u} [Ring R] : Polynomial.restriction 1 = 1

theorem Polynomial.eval₂_restriction {R : Type u} {S : Type u_1} [Ring R] [Semiring S] {f : R →+* S} {x : S} {p : Polynomial R} : Polynomial.eval₂ f x p = Polynomial.eval₂ (RingHom.comp f (Subring.subtype (Subring.closure ↑(Polynomial.frange p)))) x (Polynomial.restriction p)

def Polynomial.toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial ↥T

Given a polynomial p and a subring T that contains the coefficients of p, return the corresponding polynomial whose coefficients are in T.

Equations

• Polynomial.toSubring p T hp = Finset.sum (Polynomial.support p) fun (i : ℕ) => (Polynomial.monomial i) { val := Polynomial.coeff p i, property := ⋯ }

@[simp]

theorem Polynomial.coeff_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) {n : ℕ} : ↑(Polynomial.coeff (Polynomial.toSubring p T hp) n) = Polynomial.coeff p n

theorem Polynomial.coeff_toSubring' {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) {n : ℕ} : ↑(Polynomial.coeff (Polynomial.toSubring p T hp) n) = Polynomial.coeff p n

@[simp]

theorem Polynomial.support_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial.support (Polynomial.toSubring p T hp) = Polynomial.support p

@[simp]

theorem Polynomial.degree_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial.degree (Polynomial.toSubring p T hp) = Polynomial.degree p

@[simp]

theorem Polynomial.natDegree_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial.natDegree (Polynomial.toSubring p T hp) = Polynomial.natDegree p

@[simp]

theorem Polynomial.monic_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial.Monic (Polynomial.toSubring p T hp) ↔ Polynomial.Monic p

@[simp]

theorem Polynomial.toSubring_zero {R : Type u} [Ring R] (T : Subring R) : Polynomial.toSubring 0 T ⋯ = 0

@[simp]

theorem Polynomial.toSubring_one {R : Type u} [Ring R] (T : Subring R) : Polynomial.toSubring 1 T ⋯ = 1

@[simp]

theorem Polynomial.map_toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑(Polynomial.frange p) ⊆ ↑T) : Polynomial.map (Subring.subtype T) (Polynomial.toSubring p T hp) = p

def Polynomial.ofSubring {R : Type u} [Ring R] (T : Subring R) (p : Polynomial ↥T) : Polynomial R

Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefficients are in the ambient ring.

Equations

• Polynomial.ofSubring T p = Finset.sum (Polynomial.support p) fun (i : ℕ) => (Polynomial.monomial i) ↑(Polynomial.coeff p i)

theorem Polynomial.coeff_ofSubring {R : Type u} [Ring R] (T : Subring R) (p : Polynomial ↥T) (n : ℕ) : Polynomial.coeff (Polynomial.ofSubring T p) n = ↑(Polynomial.coeff p n)

@[simp]

theorem Polynomial.frange_ofSubring {R : Type u} [Ring R] (T : Subring R) {p : Polynomial ↥T} : ↑(Polynomial.frange (Polynomial.ofSubring T p)) ⊆ ↑T

theorem Polynomial.mem_ker_modByMonic {R : Type u} [CommRing R] {q : Polynomial R} (hq : Polynomial.Monic q) {p : Polynomial R} : p ∈ LinearMap.ker (Polynomial.modByMonicHom q) ↔ q ∣ p

@[simp]

theorem Polynomial.ker_modByMonicHom {R : Type u} [CommRing R] {q : Polynomial R} (hq : Polynomial.Monic q) : LinearMap.ker (Polynomial.modByMonicHom q) = Submodule.restrictScalars R (Ideal.span {q})

def Ideal.ofPolynomial {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) : Submodule R (Polynomial R)

Transport an ideal of R[X] to an R-submodule of R[X].

Equations

• Ideal.ofPolynomial I = { toAddSubmonoid := { toAddSubsemigroup := { carrier := I.carrier, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

theorem Ideal.mem_ofPolynomial {R : Type u} [Semiring R] {I : Ideal (Polynomial R)} (x : Polynomial R) : x ∈ Ideal.ofPolynomial I ↔ x ∈ I

def Ideal.degreeLE {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : WithBot ℕ) : Submodule R (Polynomial R)

Given an ideal I of R[X], make the R-submodule of I consisting of polynomials of degree ≤ n.

Equations

• Ideal.degreeLE I n = Polynomial.degreeLE R n ⊓ Ideal.ofPolynomial I

def Ideal.leadingCoeffNth {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) (n : ℕ) : Ideal R

Given an ideal I of R[X], make the ideal in R of leading coefficients of polynomials in I with degree ≤ n.

Equations

• Ideal.leadingCoeffNth I n = Submodule.map (Polynomial.lcoeff R n) (Ideal.degreeLE I ↑n)

def Ideal.leadingCoeff {R : Type u} [Semiring R] (I : Ideal (Polynomial R)) : Ideal R

Given an ideal I in R[X], make the ideal in R of the leading coefficients in I.

Equations

• Ideal.leadingCoeff I = ⨆ (n : ℕ), Ideal.leadingCoeffNth I n

theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R) (hp : ∀ (n : ℕ), Polynomial.coeff p n ∈ Ideal.comap Polynomial.C I) : p ∈ I

If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself

theorem Ideal.mem_map_C_iff {R : Type u} [CommSemiring R] {I : Ideal R} {f : Polynomial R} : f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), Polynomial.coeff f n ∈ I

The push-forward of an ideal I of R to R[X] via inclusion is exactly the set of polynomials whose coefficients are in I

theorem Polynomial.ker_mapRingHom {R : Type u} {S : Type u_1} [CommSemiring R] [Semiring S] (f : R →+* S) : LinearMap.ker (RingHom.toSemilinearMap (Polynomial.mapRingHom f)) = Ideal.map Polynomial.C (RingHom.ker f)

theorem Ideal.mem_leadingCoeffNth {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (n : ℕ) (x : R) : x ∈ Ideal.leadingCoeffNth I n ↔ ∃ p ∈ I, Polynomial.degree p ≤ ↑n ∧ Polynomial.leadingCoeff p = x

theorem Ideal.mem_leadingCoeffNth_zero {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ Ideal.leadingCoeffNth I 0 ↔ Polynomial.C x ∈ I

theorem Ideal.leadingCoeffNth_mono {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) {m : ℕ} {n : ℕ} (H : m ≤ n) : Ideal.leadingCoeffNth I m ≤ Ideal.leadingCoeffNth I n

theorem Ideal.mem_leadingCoeff {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ Ideal.leadingCoeff I ↔ ∃ p ∈ I, Polynomial.leadingCoeff p = x

theorem Polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial R) (I : Ideal R) (n : ι → ℕ) (h : ∀ i ∈ s, ∀ (k : ℕ), Polynomial.coeff (f i) k ∈ I ^ (n i - k)) (k : ℕ) : Polynomial.coeff (Finset.prod s f) k ∈ I ^ (Finset.sum s n - k)

If I is an ideal, and pᵢ is a finite family of polynomials each satisfying ∀ k, (pᵢ)ₖ ∈ Iⁿⁱ⁻ᵏ for some nᵢ, then p = ∏ pᵢ also satisfies ∀ k, pₖ ∈ Iⁿ⁻ᵏ with n = ∑ nᵢ.

theorem Ideal.polynomial_not_isField {R : Type u} [Ring R] : ¬IsField (Polynomial R)

R[X] is never a field for any ring R.

theorem Ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [Ring R] (hR : IsField R) (I : Ideal (Polynomial R)) [hI : Ideal.IsMaximal I] (x : R) (hx : Polynomial.C x ∈ I) : x = 0

The only constant in a maximal ideal over a field is 0.

theorem Ideal.isPrime_map_C_iff_isPrime {R : Type u} [CommRing R] (P : Ideal R) : Ideal.IsPrime (Ideal.map Polynomial.C P) ↔ Ideal.IsPrime P

If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

theorem Ideal.isPrime_map_C_of_isPrime {R : Type u} [CommRing R] {P : Ideal R} (H : Ideal.IsPrime P) : Ideal.IsPrime (Ideal.map Polynomial.C P)

If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].

theorem Ideal.is_fg_degreeLE {R : Type u} [CommRing R] [IsNoetherianRing R] (I : Ideal (Polynomial R)) (n : ℕ) : Submodule.FG (Ideal.degreeLE I ↑n)

theorem Polynomial.prime_C_iff {R : Type u} [CommRing R] {r : R} : Prime (Polynomial.C r) ↔ Prime r

theorem MvPolynomial.prime_C_iff {R : Type u} (σ : Type v) [CommRing R] {r : R} : Prime (MvPolynomial.C r) ↔ Prime r

theorem MvPolynomial.prime_rename_iff {R : Type u} {σ : Type v} [CommRing R] (s : Set σ) {p : MvPolynomial (↑s) R} : Prime ((MvPolynomial.rename Subtype.val) p) ↔ Prime p

instance Polynomial.wfDvdMonoid {R : Type u_2} [CommRing R] [IsDomain R] [WfDvdMonoid R] : WfDvdMonoid (Polynomial R)

Equations

• ⋯ = ⋯

theorem Polynomial.isNoetherianRing {R : Type u} [CommRing R] [inst : IsNoetherianRing R] : IsNoetherianRing (Polynomial R)

Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring.

theorem Polynomial.exists_irreducible_of_degree_pos {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : 0 < Polynomial.degree f) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

theorem Polynomial.exists_irreducible_of_natDegree_pos {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : 0 < Polynomial.natDegree f) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

theorem Polynomial.exists_irreducible_of_natDegree_ne_zero {R : Type u} [CommRing R] [IsDomain R] [WfDvdMonoid R] {f : Polynomial R} (hf : Polynomial.natDegree f ≠ 0) : ∃ (g : Polynomial R), Irreducible g ∧ g ∣ f

theorem Polynomial.linearIndependent_powers_iff_aeval {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) (v : M) : (LinearIndependent R fun (n : ℕ) => (f ^ n) v) ↔ ∀ (p : Polynomial R), ((Polynomial.aeval f) p) v = 0 → p = 0

theorem Polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p : Polynomial R} {q : Polynomial R} (hpq : IsCoprime p q) : Disjoint (LinearMap.ker ((Polynomial.aeval f) p)) (LinearMap.ker ((Polynomial.aeval f) q))

theorem Polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p : Polynomial R} {q : Polynomial R} (hpq : IsCoprime p q) : LinearMap.range ((Polynomial.aeval f) p) ⊔ LinearMap.range ((Polynomial.aeval f) q) = ⊤

theorem Polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : M →ₗ[R] M} {p : Polynomial R} {q : Polynomial R} : LinearMap.ker ((Polynomial.aeval f) p) ⊔ LinearMap.ker ((Polynomial.aeval f) q) ≤ LinearMap.ker ((Polynomial.aeval f) (p * q))

theorem Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : M →ₗ[R] M) {p : Polynomial R} {q : Polynomial R} (hpq : IsCoprime p q) : LinearMap.ker ((Polynomial.aeval f) p) ⊔ LinearMap.ker ((Polynomial.aeval f) q) = LinearMap.ker ((Polynomial.aeval f) (p * q))

theorem MvPolynomial.aeval_natDegree_le {σ : Type v} {R : Type u_2} [CommSemiring R] {m : ℕ} {n : ℕ} (F : MvPolynomial σ R) (hF : MvPolynomial.totalDegree F ≤ m) (f : σ → Polynomial R) (hf : ∀ (i : σ), Polynomial.natDegree (f i) ≤ n) : Polynomial.natDegree ((MvPolynomial.aeval f) F) ≤ m * n

theorem MvPolynomial.isNoetherianRing_fin_0 {R : Type u} [CommRing R] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial (Fin 0) R)

theorem MvPolynomial.isNoetherianRing_fin {R : Type u} [CommRing R] [IsNoetherianRing R] {n : ℕ} : IsNoetherianRing (MvPolynomial (Fin n) R)

instance MvPolynomial.isNoetherianRing {R : Type u} {σ : Type v} [CommRing R] [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)

The multivariate polynomial ring in finitely many variables over a noetherian ring is itself a noetherian ring.

Equations

• ⋯ = ⋯

theorem MvPolynomial.noZeroDivisors_fin (R : Type u) [CommSemiring R] [NoZeroDivisors R] (n : ℕ) : NoZeroDivisors (MvPolynomial (Fin n) R)

Auxiliary lemma: Multivariate polynomials over an integral domain with variables indexed by Fin n form an integral domain. This fact is proven inductively, and then used to prove the general case without any finiteness hypotheses. See MvPolynomial.noZeroDivisors for the general case.

theorem MvPolynomial.noZeroDivisors_of_finite (R : Type u) (σ : Type v) [CommSemiring R] [Finite σ] [NoZeroDivisors R] : NoZeroDivisors (MvPolynomial σ R)

Auxiliary definition: Multivariate polynomials in finitely many variables over an integral domain form an integral domain. This fact is proven by transport of structure from the MvPolynomial.noZeroDivisors_fin, and then used to prove the general case without finiteness hypotheses. See MvPolynomial.noZeroDivisors for the general case.

instance MvPolynomial.instNoZeroDivisorsMvPolynomialToMulToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringCommSemiringToZeroToCommMonoidWithZero {R : Type u} [CommSemiring R] [NoZeroDivisors R] {σ : Type v} : NoZeroDivisors (MvPolynomial σ R)

Equations

• ⋯ = ⋯

instance MvPolynomial.isDomain {R : Type u} {σ : Type v} [CommRing R] [IsDomain R] : IsDomain (MvPolynomial σ R)

The multivariate polynomial ring over an integral domain is an integral domain.

Equations

• ⋯ = ⋯

theorem MvPolynomial.map_mvPolynomial_eq_eval₂ {R : Type u} {σ : Type v} [CommRing R] {S : Type u_2} [CommRing S] [Finite σ] (ϕ : MvPolynomial σ R →+* S) (p : MvPolynomial σ R) : ϕ p = MvPolynomial.eval₂ (RingHom.comp ϕ MvPolynomial.C) (fun (s : σ) => ϕ (MvPolynomial.X s)) p

theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [CommRing R] (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R) (hcoe : ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p ∈ Ideal.comap MvPolynomial.C I) : p ∈ I

If every coefficient of a polynomial is in an ideal I, then so is the polynomial itself, multivariate version.

theorem MvPolynomial.mem_map_C_iff {R : Type u} {σ : Type v} [CommRing R] {I : Ideal R} {f : MvPolynomial σ R} : f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I

The push-forward of an ideal I of R to MvPolynomial σ R via inclusion is exactly the set of polynomials whose coefficients are in I

theorem MvPolynomial.ker_map {R : Type u} {S : Type u_1} {σ : Type v} [CommRing R] [CommRing S] (f : R →+* S) : RingHom.ker (MvPolynomial.map f) = Ideal.map MvPolynomial.C (RingHom.ker f)

instance Polynomial.uniqueFactorizationMonoid {D : Type u} [CommRing D] [IsDomain D] [UniqueFactorizationMonoid D] : UniqueFactorizationMonoid (Polynomial D)

Equations

• ⋯ = ⋯

noncomputable def Polynomial.fintypeSubtypeMonicDvd {D : Type u} [CommRing D] [IsDomain D] [UniqueFactorizationMonoid D] (f : Polynomial D) (hf : f ≠ 0) : Fintype { g : Polynomial D // Polynomial.Monic g ∧ g ∣ f }

If D is a unique factorization domain, f is a non-zero polynomial in D[X], then f has only finitely many monic factors. (Note that its factors up to unit may be more than monic factors.) See also UniqueFactorizationMonoid.fintypeSubtypeDvd.

Equations

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

instance MvPolynomial.uniqueFactorizationMonoid (σ : Type v) {D : Type u} [CommRing D] [IsDomain D] [UniqueFactorizationMonoid D] : UniqueFactorizationMonoid (MvPolynomial σ D)

Equations

• ⋯ = ⋯

theorem Polynomial.exists_monic_irreducible_factor {F : Type u_2} [Field F] (f : Polynomial F) (hu : ¬IsUnit f) : ∃ (g : Polynomial F), Polynomial.Monic g ∧ Irreducible g ∧ g ∣ f

A polynomial over a field which is not a unit must have a monic irreducible factor. See also WfDvdMonoid.exists_irreducible_factor.