mathlib documentation

ring_theory.polynomial.basic

Ring-theoretic supplement of data.polynomial. #

Main results #

source
@[protected, instance]
def polynomial.char_p {R : Type u} [semiring R] (p : ℕ) [h : char_p R p] :
char_p R[X] p
source
noncomputable def polynomial.degree_le (R : Type u) [comm_ring R] (n : with_bot ℕ) :
submodule R R[X]

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

Equations
source
noncomputable def polynomial.degree_lt (R : Type u) [comm_ring R] (n : ℕ) :
submodule R R[X]

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

Equations
source
theorem polynomial.mem_degree_le {R : Type u} [comm_ring R] {n : with_bot ℕ} {f : R[X]} :
f ∈ polynomial.degree_le R n ↔ f.degree ≤ n
source
theorem polynomial.degree_le_mono {R : Type u} [comm_ring R] {m n : with_bot ℕ} (H : m ≤ n) :
polynomial.degree_le R m ≤ polynomial.degree_le R n
source
theorem polynomial.degree_le_eq_span_X_pow {R : Type u} [comm_ring R] {n : ℕ} :
polynomial.degree_le R ↑n = submodule.span R ↑(finset.image (λ (n : ℕ), polynomial.X ^ n) (finset.range (n + 1)))
source
theorem polynomial.mem_degree_lt {R : Type u} [comm_ring R] {n : ℕ} {f : R[X]} :
f ∈ polynomial.degree_lt R n ↔ f.degree < ↑n
source
theorem polynomial.degree_lt_mono {R : Type u} [comm_ring R] {m n : ℕ} (H : m ≤ n) :
polynomial.degree_lt R m ≤ polynomial.degree_lt R n
source
theorem polynomial.degree_lt_eq_span_X_pow {R : Type u} [comm_ring R] {n : ℕ} :
polynomial.degree_lt R n = submodule.span R ↑(finset.image (λ (n : ℕ), polynomial.X ^ n) (finset.range n))
source
noncomputable def polynomial.degree_lt_equiv (R : Type u) [comm_ring R] (n : ℕ) :
↥(polynomial.degree_lt R n) ≃ₗ[R] fin n → R

The first n coefficients on degree_lt n form a linear equivalence with fin n → R.

Equations
source
noncomputable def polynomial.frange {R : Type u} [comm_ring R] (p : R[X]) :
finset R

The finset of nonzero coefficients of a polynomial.

Equations
source
theorem polynomial.frange_zero {R : Type u} [comm_ring R] :
0.frange = ∅
source
theorem polynomial.mem_frange_iff {R : Type u} [comm_ring R] {p : R[X]} {c : R} :
c ∈ p.frange ↔ ∃ (n : ℕ) (H : n ∈ p.support), c = p.coeff n
source
theorem polynomial.frange_one {R : Type u} [comm_ring R] :
1.frange ⊆ {1}
source
theorem polynomial.coeff_mem_frange {R : Type u} [comm_ring R] (p : R[X]) (n : ℕ) (h : p.coeff n ≠ 0) :
p.coeff n ∈ p.frange
source
noncomputable def polynomial.restriction {R : Type u} [comm_ring R] (p : R[X]) :
(↥(subring.closure ↑(p.frange)))[X]

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

Equations
source
@[simp]
theorem polynomial.coeff_restriction {R : Type u} [comm_ring R] {p : R[X]} {n : ℕ} :
↑(p.restriction.coeff n) = p.coeff n
source
@[simp]
theorem polynomial.coeff_restriction' {R : Type u} [comm_ring R] {p : R[X]} {n : ℕ} :
(p.restriction.coeff n).val = p.coeff n
source
@[simp]
theorem polynomial.support_restriction {R : Type u} [comm_ring R] (p : R[X]) :
p.restriction.support = p.support
source
@[simp]
theorem polynomial.map_restriction {R : Type u} [comm_ring R] (p : R[X]) :
polynomial.map (algebra_map ↥(subring.closure ↑(p.frange)) R) p.restriction = p
source
@[simp]
theorem polynomial.degree_restriction {R : Type u} [comm_ring R] {p : R[X]} :
p.restriction.degree = p.degree
source
@[simp]
theorem polynomial.nat_degree_restriction {R : Type u} [comm_ring R] {p : R[X]} :
p.restriction.nat_degree = p.nat_degree
source
@[simp]
theorem polynomial.monic_restriction {R : Type u} [comm_ring R] {p : R[X]} :
p.restriction.monic ↔ p.monic
source
@[simp]
theorem polynomial.restriction_zero {R : Type u} [comm_ring R] :
0.restriction = 0
source
@[simp]
theorem polynomial.restriction_one {R : Type u} [comm_ring R] :
1.restriction = 1
source
theorem polynomial.eval₂_restriction {R : Type u} [comm_ring R] {S : Type v} [ring S] {f : R →+* S} {x : S} {p : R[X]} :
polynomial.eval₂ f x p = polynomial.eval₂ (f.comp (subring.closure ↑(p.frange)).subtype) x p.restriction
source
theorem polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [comm_ring R] (n : ℕ) :
(geom_sum polynomial.X n).comp (polynomial.X + 1) = ∑ (i : ℕ) in finset.range n, (↑(n.choose (i + 1))) * polynomial.X ^ i
source
theorem polynomial.monic.geom_sum {R : Type u_1} [semiring R] {P : R[X]} (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : ℕ} (hn : n ≠ 0) :
(geom_sum P n).monic
source
theorem polynomial.monic.geom_sum' {R : Type u_1} [semiring R] {P : R[X]} (hP : P.monic) (hdeg : 0 < P.degree) {n : ℕ} (hn : n ≠ 0) :
(geom_sum P n).monic
source
theorem polynomial.monic_geom_sum_X (R : Type u_1) [semiring R] {n : ℕ} (hn : n ≠ 0) :
(geom_sum polynomial.X n).monic
source
noncomputable def polynomial.to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
(↥T)[X]

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

Equations
source
@[simp]
theorem polynomial.coeff_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) {n : ℕ} :
↑((p.to_subring T hp).coeff n) = p.coeff n
source
@[simp]
theorem polynomial.coeff_to_subring' {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) {n : ℕ} :
((p.to_subring T hp).coeff n).val = p.coeff n
source
@[simp]
theorem polynomial.support_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
(p.to_subring T hp).support = p.support
source
@[simp]
theorem polynomial.degree_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
(p.to_subring T hp).degree = p.degree
source
@[simp]
theorem polynomial.nat_degree_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
(p.to_subring T hp).nat_degree = p.nat_degree
source
@[simp]
theorem polynomial.monic_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
(p.to_subring T hp).monic ↔ p.monic
source
@[simp]
theorem polynomial.to_subring_zero {R : Type u} [comm_ring R] (T : subring R) :
0.to_subring T _ = 0
source
@[simp]
theorem polynomial.to_subring_one {R : Type u} [comm_ring R] (T : subring R) :
1.to_subring T _ = 1
source
@[simp]
theorem polynomial.map_to_subring {R : Type u} [comm_ring R] (p : R[X]) (T : subring R) (hp : ↑(p.frange) ⊆ ↑T) :
polynomial.map T.subtype (p.to_subring T hp) = p
source
noncomputable def polynomial.of_subring {R : Type u} [comm_ring R] (T : subring R) (p : (↥T)[X]) :
R[X]

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

Equations
source
theorem polynomial.coeff_of_subring {R : Type u} [comm_ring R] (T : subring R) (p : (↥T)[X]) (n : ℕ) :
(polynomial.of_subring T p).coeff n = ↑(p.coeff n)
source
@[simp]
theorem polynomial.frange_of_subring {R : Type u} [comm_ring R] (T : subring R) {p : (↥T)[X]} :
↑((polynomial.of_subring T p).frange) ⊆ ↑T
source
theorem polynomial.mem_ker_mod_by_monic {R : Type u} [comm_ring R] {q : R[X]} (hq : q.monic) {p : R[X]} :
p ∈ q.mod_by_monic_hom.ker ↔ q ∣ p
source
@[simp]
theorem polynomial.ker_mod_by_monic_hom {R : Type u} [comm_ring R] {q : R[X]} (hq : q.monic) :
q.mod_by_monic_hom.ker = submodule.restrict_scalars R (ideal.span {q})
source
theorem ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [comm_ring R] (I : ideal R[X]) (p : R[X]) (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

source
theorem ideal.mem_map_C_iff {R : Type u} [comm_ring R] {I : ideal R} {f : R[X]} :
f ∈ ideal.map polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I

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

source
theorem polynomial.ker_map_ring_hom {R : Type u} {S : Type u_1} [comm_ring R] [comm_ring S] (f : R →+* S) :
(polynomial.map_ring_hom f).ker = ideal.map polynomial.C f.ker
source
theorem ideal.quotient_map_C_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (a : R) (H : a ∈ I) :
⇑((ideal.quotient.mk (ideal.map polynomial.C I)).comp polynomial.C) a = 0
source
theorem ideal.eval₂_C_mk_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (f : R[X]) (H : f ∈ ideal.map polynomial.C I) :
⇑(polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) f = 0
source
noncomputable def ideal.polynomial_quotient_equiv_quotient_polynomial {R : Type u} [comm_ring R] (I : ideal R) :
(R ⧸ I)[X] ≃+* R[X] ⧸ ideal.map polynomial.C I

If I is an ideal of R, then the ring polynomials over the quotient ring I.quotient is isomorphic to the quotient of polynomial R by the ideal map C I, where map C I contains exactly the polynomials whose coefficients all lie in I

Equations
source
@[simp]
theorem ideal.polynomial_quotient_equiv_quotient_polynomial_symm_mk {R : Type u} [comm_ring R] (I : ideal R) (f : R[X]) :
⇑(I.polynomial_quotient_equiv_quotient_polynomial.symm) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f) = polynomial.map (ideal.quotient.mk I) f
source
@[simp]
theorem ideal.polynomial_quotient_equiv_quotient_polynomial_map_mk {R : Type u} [comm_ring R] (I : ideal R) (f : R[X]) :
⇑(I.polynomial_quotient_equiv_quotient_polynomial) (polynomial.map (ideal.quotient.mk I) f) = ⇑(ideal.quotient.mk (ideal.map polynomial.C I)) f
source
theorem ideal.is_domain_map_C_quotient {R : Type u} [comm_ring R] {P : ideal R} (H : P.is_prime) :
is_domain (R[X] ⧸ ideal.map polynomial.C P)

If P is a prime ideal of R, then R[x]/(P) is an integral domain.

source
theorem ideal.is_prime_map_C_of_is_prime {R : Type u} [comm_ring R] {P : ideal R} (H : P.is_prime) :
(ideal.map polynomial.C P).is_prime

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

source
theorem ideal.eq_zero_of_polynomial_mem_map_range {R : Type u} [comm_ring R] (I : ideal R[X]) (x : ↥(((ideal.quotient.mk I).comp polynomial.C).range)) (hx : ⇑polynomial.C x ∈ ideal.map (polynomial.map_ring_hom ((ideal.quotient.mk I).comp polynomial.C).range_restrict) I) :
x = 0

Given any ring R and an ideal I of polynomial R, we get a map R → R[x] → R[x]/I. If we let R be the image of R in R[x]/I then we also have a map R[x] → R'[x]. In particular we can map I across this map, to get I' and a new map R' → R'[x] → R'[x]/I. This theorem shows I' will not contain any non-zero constant polynomials

source
theorem ideal.polynomial_not_is_field {R : Type u} [comm_ring R] :
¬is_field R[X]

polynomial R is never a field for any ring R.

source
theorem ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [comm_ring R] (hR : is_field R) (I : ideal R[X]) [hI : I.is_maximal] (x : R) (hx : ⇑polynomial.C x ∈ I) :
x = 0

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

source
def ideal.of_polynomial {R : Type u} [comm_ring R] (I : ideal R[X]) :
submodule R R[X]

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

Equations
source
theorem ideal.mem_of_polynomial {R : Type u} [comm_ring R] {I : ideal R[X]} (x : R[X]) :
x ∈ I.of_polynomial ↔ x ∈ I
source
noncomputable def ideal.degree_le {R : Type u} [comm_ring R] (I : ideal R[X]) (n : with_bot ℕ) :
submodule R R[X]

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

Equations
source
noncomputable def ideal.leading_coeff_nth {R : Type u} [comm_ring R] (I : ideal R[X]) (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
source
theorem ideal.mem_leading_coeff_nth {R : Type u} [comm_ring R] (I : ideal R[X]) (n : ℕ) (x : R) :
x ∈ I.leading_coeff_nth n ↔ ∃ (p : R[X]) (H : p ∈ I), p.degree ≤ ↑n ∧ p.leading_coeff = x
source
theorem ideal.mem_leading_coeff_nth_zero {R : Type u} [comm_ring R] (I : ideal R[X]) (x : R) :
x ∈ I.leading_coeff_nth 0 ↔ ⇑polynomial.C x ∈ I
source
theorem ideal.leading_coeff_nth_mono {R : Type u} [comm_ring R] (I : ideal R[X]) {m n : ℕ} (H : m ≤ n) :
I.leading_coeff_nth m ≤ I.leading_coeff_nth n
source
noncomputable def ideal.leading_coeff {R : Type u} [comm_ring R] (I : ideal R[X]) :
ideal R

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

Equations
source
theorem ideal.mem_leading_coeff {R : Type u} [comm_ring R] (I : ideal R[X]) (x : R) :
x ∈ I.leading_coeff ↔ ∃ (p : R[X]) (H : p ∈ I), p.leading_coeff = x
source
theorem ideal.is_fg_degree_le {R : Type u} [comm_ring R] (I : ideal R[X]) [is_noetherian_ring R] (n : ℕ) :
(I.degree_le ↑n).fg
source
theorem polynomial.prime_C_iff {R : Type u} [comm_ring R] {r : R} :
prime (⇑polynomial.C r) ↔ prime r
source
theorem mv_polynomial.prime_C_iff {R : Type u} (σ : Type v) [comm_ring R] {r : R} :
prime (⇑mv_polynomial.C r) ↔ prime r
source
theorem mv_polynomial.prime_rename_iff {R : Type u} {σ : Type v} [comm_ring R] (s : set σ) {p : mv_polynomial ↥s R} :
prime (⇑(mv_polynomial.rename coe) p) ↔ prime p
source
@[protected, instance]
def polynomial.wf_dvd_monoid {R : Type u_1} [comm_ring R] [is_domain R] [wf_dvd_monoid R] :
wf_dvd_monoid R[X]
source
@[protected, instance]
theorem polynomial.is_noetherian_ring {R : Type u} [comm_ring R] [is_noetherian_ring R] :
is_noetherian_ring R[X]

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

source
theorem polynomial.exists_irreducible_of_degree_pos {R : Type u} [comm_ring R] [is_domain R] [wf_dvd_monoid R] {f : R[X]} (hf : 0 < f.degree) :
∃ (g : R[X]), irreducible g ∧ g ∣ f
source
theorem polynomial.exists_irreducible_of_nat_degree_pos {R : Type u} [comm_ring R] [is_domain R] [wf_dvd_monoid R] {f : R[X]} (hf : 0 < f.nat_degree) :
∃ (g : R[X]), irreducible g ∧ g ∣ f
source
theorem polynomial.exists_irreducible_of_nat_degree_ne_zero {R : Type u} [comm_ring R] [is_domain R] [wf_dvd_monoid R] {f : R[X]} (hf : f.nat_degree ≠ 0) :
∃ (g : R[X]), irreducible g ∧ g ∣ f
source
theorem polynomial.linear_independent_powers_iff_aeval {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) (v : M) :
linear_independent R (λ (n : ℕ), ⇑(f ^ n) v) ↔ ∀ (p : R[X]), ⇑(⇑(polynomial.aeval f) p) v = 0 → p = 0
source
theorem polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : R[X]} (hpq : is_coprime p q) :
disjoint (⇑(polynomial.aeval f) p).ker (⇑(polynomial.aeval f) q).ker
source
theorem polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : R[X]} (hpq : is_coprime p q) :
(⇑(polynomial.aeval f) p).range ⊔ (⇑(polynomial.aeval f) q).range = ⊤
source
theorem polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] {f : M →ₗ[R] M} {p q : R[X]} :
(⇑(polynomial.aeval f) p).ker ⊔ (⇑(polynomial.aeval f) q).ker ≤ (⇑(polynomial.aeval f) (p * q)).ker
source
theorem polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) {p q : R[X]} (hpq : is_coprime p q) :
(⇑(polynomial.aeval f) p).ker ⊔ (⇑(polynomial.aeval f) q).ker = (⇑(polynomial.aeval f) (p * q)).ker
source
theorem mv_polynomial.is_noetherian_ring_fin_0 {R : Type u} [comm_ring R] [is_noetherian_ring R] :
is_noetherian_ring (mv_polynomial (fin 0) R)
source
theorem mv_polynomial.is_noetherian_ring_fin {R : Type u} [comm_ring R] [is_noetherian_ring R] {n : ℕ} :
is_noetherian_ring (mv_polynomial (fin n) R)
source
@[protected, instance]
def mv_polynomial.is_noetherian_ring {R : Type u} {σ : Type v} [comm_ring R] [fintype σ] [is_noetherian_ring R] :
is_noetherian_ring (mv_polynomial σ R)

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

source
theorem mv_polynomial.is_domain_fin_zero (R : Type u) [comm_ring R] [is_domain R] :
is_domain (mv_polynomial (fin 0) R)
source
theorem mv_polynomial.is_domain_fin (R : Type u) [comm_ring R] [is_domain R] (n : ℕ) :
is_domain (mv_polynomial (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 mv_polynomial.is_domain for the general case.

source
theorem mv_polynomial.is_domain_fintype (R : Type u) (σ : Type v) [comm_ring R] [fintype σ] [is_domain R] :
is_domain (mv_polynomial σ 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 mv_polynomial.is_domain_fin, and then used to prove the general case without finiteness hypotheses. See mv_polynomial.is_domain for the general case.

source
@[protected]
theorem mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero {R : Type u} [comm_ring R] [is_domain R] {σ : Type v} (p q : mv_polynomial σ R) (h : p * q = 0) :
p = 0 ∨ q = 0
source
@[protected, instance]
def mv_polynomial.is_domain {R : Type u} {σ : Type v} [comm_ring R] [is_domain R] :
is_domain (mv_polynomial σ R)

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

source
theorem mv_polynomial.map_mv_polynomial_eq_eval₂ {R : Type u} {σ : Type v} [comm_ring R] {S : Type u_1} [comm_ring S] [fintype σ] (ϕ : mv_polynomial σ R →+* S) (p : mv_polynomial σ R) :
⇑ϕ p = mv_polynomial.eval₂ (ϕ.comp mv_polynomial.C) (λ (s : σ), ⇑ϕ (mv_polynomial.X s)) p
source
theorem mv_polynomial.quotient_map_C_eq_zero {R : Type u} {σ : Type v} [comm_ring R] {I : ideal R} {i : R} (hi : i ∈ I) :
⇑((ideal.quotient.mk (ideal.map mv_polynomial.C I)).comp mv_polynomial.C) i = 0
source
theorem mv_polynomial.mem_ideal_of_coeff_mem_ideal {R : Type u} {σ : Type v} [comm_ring R] (I : ideal (mv_polynomial σ R)) (p : mv_polynomial σ R) (hcoe : ∀ (m : σ →₀ ℕ), mv_polynomial.coeff m p ∈ ideal.comap mv_polynomial.C I) :
p ∈ I

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

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

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

source
theorem mv_polynomial.ker_map {R : Type u} {S : Type u_1} {σ : Type v} [comm_ring R] [comm_ring S] (f : R →+* S) :
(mv_polynomial.map f).ker = ideal.map mv_polynomial.C f.ker
source
theorem mv_polynomial.eval₂_C_mk_eq_zero {R : Type u} {σ : Type v} [comm_ring R] {I : ideal R} {a : mv_polynomial σ R} (ha : a ∈ ideal.map mv_polynomial.C I) :
⇑(mv_polynomial.eval₂_hom (mv_polynomial.C.comp (ideal.quotient.mk I)) mv_polynomial.X) a = 0
source
noncomputable def mv_polynomial.quotient_equiv_quotient_mv_polynomial {R : Type u} {σ : Type v} [comm_ring R] (I : ideal R) :
mv_polynomial σ (R ⧸ I) ≃ₐ[R] mv_polynomial σ R ⧸ ideal.map mv_polynomial.C I

If I is an ideal of R, then the ring mv_polynomial σ I.quotient is isomorphic as an R-algebra to the quotient of mv_polynomial σ R by the ideal generated by I.

Equations
source
@[protected, instance]
def polynomial.unique_factorization_monoid {D : Type u} [comm_ring D] [is_domain D] [unique_factorization_monoid D] :
unique_factorization_monoid D[X]
source
@[protected, instance]
def mv_polynomial.unique_factorization_monoid (σ : Type v) {D : Type u} [comm_ring D] [is_domain D] [unique_factorization_monoid D] :
unique_factorization_monoid (mv_polynomial σ D)