ring_theory.polynomial.basic

source

@[protected, instance]

def polynomial.char_p {R : Type u} [semiring R] (p : ℕ) [h : char_p R p] :

char_p (polynomial R) p

source

noncomputable def polynomial.degree_le (R : Type u) [semiring R] (n : with_bot ℕ) :

submodule R (polynomial R)

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

Equations

polynomial.degree_le R n = ⨅ (k : ℕ) (h : ↑k > n), linear_map.ker (polynomial.lcoeff R k)

source

noncomputable def polynomial.degree_lt (R : Type u) [semiring R] (n : ℕ) :

submodule R (polynomial R)

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

Equations

polynomial.degree_lt R n = ⨅ (k : ℕ) (h : k ≥ n), linear_map.ker (polynomial.lcoeff R k)

source

theorem polynomial.mem_degree_le {R : Type u} [semiring R] {n : with_bot ℕ} {f : polynomial R} :

f ∈ polynomial.degree_le R n ↔ f.degree ≤ n

source

theorem polynomial.degree_le_mono {R : Type u} [semiring 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} [semiring 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} [semiring R] {n : ℕ} {f : polynomial R} :

f ∈ polynomial.degree_lt R n ↔ f.degree < ↑n

source

theorem polynomial.degree_lt_mono {R : Type u} [semiring 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} [semiring 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_1) [semiring 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

polynomial.degree_lt_equiv R n = {to_fun := λ (p : ↥(polynomial.degree_lt R n)) (n_1 : fin n), ↑p.coeff ↑n_1, map_add' := _, map_smul' := _, inv_fun := λ (f : fin n → R), ⟨finset.univ.sum (λ (i : fin n), ⇑(polynomial.monomial ↑i) (f i)), _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem polynomial.degree_lt_equiv_eq_zero_iff_eq_zero {R : Type u} [semiring R] {n : ℕ} {p : polynomial R} (hp : p ∈ polynomial.degree_lt R n) :

⇑(polynomial.degree_lt_equiv R n) ⟨p, hp⟩ = 0 ↔ p = 0

source

theorem polynomial.eval_eq_sum_degree_lt_equiv {R : Type u} [semiring R] {n : ℕ} {p : polynomial R} (hp : p ∈ polynomial.degree_lt R n) (x : R) :

polynomial.eval x p = finset.univ.sum (λ (i : fin n), ⇑(polynomial.degree_lt_equiv R n) ⟨p, hp⟩ i * x ^ ↑i)

source

noncomputable def polynomial.frange {R : Type u} [semiring R] (p : polynomial R) :

finset R

The finset of nonzero coefficients of a polynomial.

Equations

p.frange = finset.image (λ (n : ℕ), p.coeff n) p.support

source

theorem polynomial.frange_zero {R : Type u} [semiring R] :

0.frange = ∅

source

theorem polynomial.mem_frange_iff {R : Type u} [semiring R] {p : polynomial R} {c : R} :

c ∈ p.frange ↔ ∃ (n : ℕ) (H : n ∈ p.support), c = p.coeff n

source

theorem polynomial.frange_one {R : Type u} [semiring R] :

1.frange ⊆ {1}

source

theorem polynomial.coeff_mem_frange {R : Type u} [semiring R] (p : polynomial R) (n : ℕ) (h : p.coeff n ≠ 0) :

p.coeff n ∈ p.frange

source

theorem polynomial.geom_sum_X_comp_X_add_one_eq_sum {R : Type u} [semiring R] (n : ℕ) :

((finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)).comp (polynomial.X + 1) = (finset.range n).sum (λ (i : ℕ), ↑(n.choose (i + 1)) * polynomial.X ^ i)

source

theorem polynomial.monic.geom_sum {R : Type u} [semiring R] {P : polynomial R} (hP : P.monic) (hdeg : 0 < P.nat_degree) {n : ℕ} (hn : n ≠ 0) :

((finset.range n).sum (λ (i : ℕ), P ^ i)).monic

source

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 (λ (i : ℕ), P ^ i)).monic

source

theorem polynomial.monic_geom_sum_X {R : Type u} [semiring R] {n : ℕ} (hn : n ≠ 0) :

((finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)).monic

source

noncomputable def polynomial.restriction {R : Type u} [ring R] (p : polynomial R) :

polynomial ↥(subring.closure ↑(p.frange))

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

Equations

p.restriction = p.support.sum (λ (i : ℕ), ⇑(polynomial.monomial i) ⟨p.coeff i, _⟩)

source

@[simp]

theorem polynomial.coeff_restriction {R : Type u} [ring R] {p : polynomial R} {n : ℕ} :

↑(p.restriction.coeff n) = p.coeff n

source

@[simp]

theorem polynomial.coeff_restriction' {R : Type u} [ring R] {p : polynomial R} {n : ℕ} :

(p.restriction.coeff n).val = p.coeff n

source

@[simp]

theorem polynomial.support_restriction {R : Type u} [ring R] (p : polynomial R) :

p.restriction.support = p.support

source

@[simp]

theorem polynomial.map_restriction {R : Type u} [comm_ring R] (p : polynomial R) :

polynomial.map (algebra_map ↥(subring.closure ↑(p.frange)) R) p.restriction = p

source

@[simp]

theorem polynomial.degree_restriction {R : Type u} [ring R] {p : polynomial R} :

p.restriction.degree = p.degree

source

@[simp]

theorem polynomial.nat_degree_restriction {R : Type u} [ring R] {p : polynomial R} :

p.restriction.nat_degree = p.nat_degree

source

@[simp]

theorem polynomial.monic_restriction {R : Type u} [ring R] {p : polynomial R} :

p.restriction.monic ↔ p.monic

source

@[simp]

theorem polynomial.restriction_zero {R : Type u} [ring R] :

0.restriction = 0

source

@[simp]

theorem polynomial.restriction_one {R : Type u} [ring R] :

1.restriction = 1

source

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.frange)).subtype) x p.restriction

source

noncomputable def polynomial.to_subring {R : Type u} [ring R] (p : polynomial R) (T : subring R) (hp : ↑(p.frange) ⊆ ↑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.to_subring T hp = p.support.sum (λ (i : ℕ), ⇑(polynomial.monomial i) ⟨p.coeff i, _⟩)

source

@[simp]

theorem polynomial.coeff_to_subring {R : Type u} [ring R] (p : polynomial R) (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} [ring R] (p : polynomial R) (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} [ring R] (p : polynomial R) (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} [ring R] (p : polynomial R) (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} [ring R] (p : polynomial R) (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} [ring R] (p : polynomial R) (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} [ring R] (T : subring R) :

0.to_subring T _ = 0

source

@[simp]

theorem polynomial.to_subring_one {R : Type u} [ring R] (T : subring R) :

1.to_subring T _ = 1

source

@[simp]

theorem polynomial.map_to_subring {R : Type u} [ring R] (p : polynomial R) (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} [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.of_subring T p = p.support.sum (λ (i : ℕ), ⇑(polynomial.monomial i) ↑(p.coeff i))

source

theorem polynomial.coeff_of_subring {R : Type u} [ring R] (T : subring R) (p : polynomial ↥T) (n : ℕ) :

(polynomial.of_subring T p).coeff n = ↑(p.coeff n)

source

@[simp]

theorem polynomial.frange_of_subring {R : Type u} [ring R] (T : subring R) {p : polynomial ↥T} :

↑((polynomial.of_subring T p).frange) ⊆ ↑T

source

theorem polynomial.mem_ker_mod_by_monic {R : Type u} [comm_ring R] {q : polynomial R} (hq : q.monic) {p : polynomial R} :

p ∈ linear_map.ker q.mod_by_monic_hom ↔ q ∣ p

source

@[simp]

theorem polynomial.ker_mod_by_monic_hom {R : Type u} [comm_ring R] {q : polynomial R} (hq : q.monic) :

linear_map.ker q.mod_by_monic_hom = submodule.restrict_scalars R (ideal.span {q})

source

def ideal.of_polynomial {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.of_polynomial = {carrier := I.carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}

source

theorem ideal.mem_of_polynomial {R : Type u} [semiring R] {I : ideal (polynomial R)} (x : polynomial R) :

x ∈ I.of_polynomial ↔ x ∈ I

source

noncomputable def ideal.degree_le {R : Type u} [semiring R] (I : ideal (polynomial R)) (n : with_bot ℕ) :

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.degree_le n = polynomial.degree_le R n ⊓ I.of_polynomial

source

noncomputable def ideal.leading_coeff_nth {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.leading_coeff_nth n = submodule.map (polynomial.lcoeff R n) (I.degree_le ↑n)

source

noncomputable def ideal.leading_coeff {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.leading_coeff = ⨆ (n : ℕ), I.leading_coeff_nth n

source

theorem ideal.polynomial_mem_ideal_of_coeff_mem_ideal {R : Type u} [comm_semiring 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

source

theorem ideal.mem_map_C_iff {R : Type u} [comm_semiring 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

source

theorem polynomial.ker_map_ring_hom {R : Type u} {S : Type u_1} [comm_semiring R] [semiring S] (f : R →+* S) :

ring_hom.ker (polynomial.map_ring_hom f) = ideal.map polynomial.C (ring_hom.ker f)

source

theorem ideal.mem_leading_coeff_nth {R : Type u} [comm_semiring R] (I : ideal (polynomial R)) (n : ℕ) (x : R) :

x ∈ I.leading_coeff_nth n ↔ ∃ (p : polynomial R) (H : p ∈ I), p.degree ≤ ↑n ∧ p.leading_coeff = x

source

theorem ideal.mem_leading_coeff_nth_zero {R : Type u} [comm_semiring R] (I : ideal (polynomial R)) (x : R) :

x ∈ I.leading_coeff_nth 0 ↔ ⇑polynomial.C x ∈ I

source

theorem ideal.leading_coeff_nth_mono {R : Type u} [comm_semiring R] (I : ideal (polynomial R)) {m n : ℕ} (H : m ≤ n) :

I.leading_coeff_nth m ≤ I.leading_coeff_nth n

source

theorem ideal.mem_leading_coeff {R : Type u} [comm_semiring R] (I : ideal (polynomial R)) (x : R) :

x ∈ I.leading_coeff ↔ ∃ (p : polynomial R) (H : p ∈ I), p.leading_coeff = x

source

theorem polynomial.coeff_prod_mem_ideal_pow_tsub {R : Type u} [comm_semiring R] {ι : Type u_1} (s : finset ι) (f : ι → polynomial R) (I : ideal R) (n : ι → ℕ) (h : ∀ (i : ι), 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ᵢ.

source

theorem ideal.polynomial_not_is_field {R : Type u} [ring R] :

¬is_field (polynomial R)

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

source

theorem ideal.eq_zero_of_constant_mem_of_maximal {R : Type u} [ring R] (hR : is_field R) (I : ideal (polynomial R)) [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

theorem ideal.is_prime_map_C_iff_is_prime {R : Type u} [comm_ring R] (P : ideal R) :

(ideal.map polynomial.C P).is_prime ↔ 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.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.is_fg_degree_le {R : Type u} [comm_ring R] [is_noetherian_ring R] (I : ideal (polynomial 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 (polynomial R)

source

@[protected, instance]

theorem polynomial.is_noetherian_ring {R : Type u} [comm_ring R] [is_noetherian_ring R] :

is_noetherian_ring (polynomial R)

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 : polynomial R} (hf : 0 < f.degree) :

∃ (g : polynomial R), 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 : polynomial R} (hf : 0 < f.nat_degree) :

∃ (g : polynomial R), 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 : polynomial R} (hf : f.nat_degree ≠ 0) :

∃ (g : polynomial R), 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 : polynomial R), ⇑(⇑(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 : polynomial R} (hpq : is_coprime p q) :

disjoint (linear_map.ker (⇑(polynomial.aeval f) p)) (linear_map.ker (⇑(polynomial.aeval f) q))

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 : polynomial R} (hpq : is_coprime p q) :

linear_map.range (⇑(polynomial.aeval f) p) ⊔ linear_map.range (⇑(polynomial.aeval f) q) = ⊤

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 : polynomial R} :

linear_map.ker (⇑(polynomial.aeval f) p) ⊔ linear_map.ker (⇑(polynomial.aeval f) q) ≤ linear_map.ker (⇑(polynomial.aeval f) (p * q))

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 : polynomial R} (hpq : is_coprime p q) :

linear_map.ker (⇑(polynomial.aeval f) p) ⊔ linear_map.ker (⇑(polynomial.aeval f) q) = linear_map.ker (⇑(polynomial.aeval f) (p * q))

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] [finite σ] [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.no_zero_divisors_fin (R : Type u) [comm_semiring R] [no_zero_divisors R] (n : ℕ) :

no_zero_divisors (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.no_zero_divisors for the general case.

source

theorem mv_polynomial.no_zero_divisors_of_finite (R : Type u) (σ : Type v) [comm_semiring R] [finite σ] [no_zero_divisors R] :

no_zero_divisors (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.no_zero_divisors_fin, and then used to prove the general case without finiteness hypotheses. See mv_polynomial.no_zero_divisors for the general case.

source

@[protected, instance]

def mv_polynomial.no_zero_divisors {R : Type u} [comm_semiring R] [no_zero_divisors R] {σ : Type v} :

no_zero_divisors (mv_polynomial σ R)

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] [finite σ] (ϕ : 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.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) :

ring_hom.ker (mv_polynomial.map f) = ideal.map mv_polynomial.C (ring_hom.ker f)

source

@[protected, instance]

def polynomial.unique_factorization_monoid {D : Type u} [comm_ring D] [is_domain D] [unique_factorization_monoid D] :

unique_factorization_monoid (polynomial D)

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)

mathlib3 documentation

Ring-theoretic supplement of data.polynomial. #

Main results #