Ring-theoretic supplement of Algebra.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 ↔ f.degree ≤ 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 ↔ f.degree < ↑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) ⟨p, 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.univ.sum fun (i : Fin n) => (Polynomial.degreeLTEquiv R n) ⟨p, 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 : s.Nonempty) (hp : p ∈ Submodule.span R s) : ∃ p' ∈ s, p.degree ≤ p'.degree

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 : s.Finite) (hs : s.Nonempty) : ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree

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 : s.Finite) : ∃ (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 : s.Finite) : ∃ (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.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

@[deprecated Polynomial.coeffs]

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

Alias of Polynomial.coeffs.

---

The finset of nonzero coefficients of a polynomial.

Equations

• @Polynomial.frange = @Polynomial.coeffs

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

@[deprecated Polynomial.coeffs_zero]

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

Alias of Polynomial.coeffs_zero.

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

@[deprecated Polynomial.mem_coeffs_iff]

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

Alias of Polynomial.mem_coeffs_iff.

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

@[deprecated Polynomial.coeffs_one]

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

Alias of Polynomial.coeffs_one.

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

@[deprecated Polynomial.coeff_mem_coeffs]

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

Alias of Polynomial.coeff_mem_coeffs.

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

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

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

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

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

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

Equations

• p.restriction = p.support.sum fun (i : ℕ) => (Polynomial.monomial i) ⟨p.coeff i, ⋯⟩

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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₂ (f.comp (Subring.closure ↑p.coeffs).subtype) x p.restriction

def Polynomial.toSubring {R : Type u} [Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.coeffs ⊆ ↑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

• p.toSubring T hp = p.support.sum fun (i : ℕ) => (Polynomial.monomial i) ⟨p.coeff i, ⋯⟩

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 : ↑p.coeffs ⊆ ↑T) : Polynomial.map T.subtype (p.toSubring 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 = p.support.sum fun (i : ℕ) => (Polynomial.monomial i) ↑(p.coeff i)

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

@[simp]

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

@[deprecated Polynomial.coeffs_ofSubring]

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

Alias of Polynomial.coeffs_ofSubring.

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

@[simp]

theorem Polynomial.ker_modByMonicHom {R : Type u} [CommRing R] {q : Polynomial R} (hq : q.Monic) : LinearMap.ker q.modByMonicHom = 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

• I.ofPolynomial = { 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 ∈ I.ofPolynomial ↔ 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

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

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

• I.leadingCoeffNth n = Submodule.map (Polynomial.lcoeff R n) (I.degreeLE ↑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

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

theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R) (hp : ∀ (n : ℕ), p.coeff 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 : ℕ), f.coeff 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 (Polynomial.mapRingHom f).toSemilinearMap = Ideal.map Polynomial.C (RingHom.ker f)

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

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

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

theorem Ideal.mem_leadingCoeff {R : Type u} [CommSemiring R] (I : Ideal (Polynomial R)) (x : R) : x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = 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 : ℕ), (f i).coeff k ∈ I ^ (n i - k)) (k : ℕ) : (s.prod f).coeff k ∈ I ^ (s.sum 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 : I.IsMaximal] (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.map Polynomial.C P).IsPrime ↔ P.IsPrime

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 : P.IsPrime) : (Ideal.map Polynomial.C P).IsPrime

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 : ℕ) : (I.degreeLE ↑n).FG

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 100]

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 < f.degree) : ∃ (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 < f.natDegree) : ∃ (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 : f.natDegree ≠ 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 : F.totalDegree ≤ m) (f : σ → Polynomial R) (hf : ∀ (i : σ), (f i).natDegree ≤ n) : ((MvPolynomial.aeval f) F).natDegree ≤ 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.instNoZeroDivisors {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₂ (ϕ.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 100]

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 // g.Monic ∧ 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 100]

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), g.Monic ∧ 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.