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.instCharPPolynomialToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringSemiring {R : Type u} [Semiring R] (p : ℕ) [h : CharP R p] : CharP (Polynomial R) p

Equations

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

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] {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] {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 : ℕ) : { x // x ∈ 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 => ↑(Polynomial.degreeLTEquiv R n) { val := p, property := hp } i * x ^ ↑i

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, 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 { x // x ∈ Subring.closure ↑(Polynomial.frange p) }

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

Equations

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

@[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 { x // x ∈ 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 { x // x ∈ 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 := (_ : Polynomial.coeff p i ∈ T) }

@[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 (_ : ↑∅ ⊆ ↑T) = 0

@[simp]

theorem Polynomial.toSubring_one {R : Type u} [Ring R] (T : Subring R) : Polynomial.toSubring 1 T (_ : ↑(Polynomial.frange 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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

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

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, 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, 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 : ι), 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.instWfDvdMonoidPolynomialToSemiringToCommSemiringToCommMonoidWithZeroCommSemiring {R : Type u_2} [CommRing R] [IsDomain R] [WfDvdMonoid R] : WfDvdMonoid (Polynomial R)

Equations

• @Polynomial.instWfDvdMonoidPolynomialToSemiringToCommSemiringToCommMonoidWithZeroCommSemiring = @Polynomial.instWfDvdMonoidPolynomialToSemiringToCommSemiringToCommMonoidWithZeroCommSemiring.proof_1

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

• @MvPolynomial.isNoetherianRing = @MvPolynomial.isNoetherianRing.proof_1

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

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

instance MvPolynomial.instIsDomainMvPolynomialToCommSemiringToSemiringCommSemiring {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

• @MvPolynomial.instIsDomainMvPolynomialToCommSemiringToSemiringCommSemiring = @MvPolynomial.instIsDomainMvPolynomialToCommSemiringToSemiringCommSemiring.proof_1

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

• @Polynomial.uniqueFactorizationMonoid = @Polynomial.uniqueFactorizationMonoid.proof_1

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

Equations

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