Ring-theoretic supplement of data.polynomial. #
Main results #
mv_polynomial.is_domain: If a ring is an integral domain, then so is its polynomial ring over finitely many variables.polynomial.is_noetherian_ring: Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.polynomial.wf_dvd_monoid: If an integral domain is awf_dvd_monoid, then so is its polynomial ring.polynomial.unique_factorization_monoid,mv_polynomial.unique_factorization_monoid: If an integral domain is aunique_factorization_monoid, then so is its polynomial ring (of any number of variables).
@[protected, instance]
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)
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)
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
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)))
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))
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.
@[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) :
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)
The finset of nonzero coefficients of a polynomial.
theorem
polynomial.coeff_mem_frange
{R : Type u}
[semiring R]
(p : polynomial R)
(n : ℕ)
(h : p.coeff n ≠ 0) :
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)
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
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
theorem
polynomial.monic_geom_sum_X
{R : Type u}
[semiring R]
{n : ℕ}
(hn : n ≠ 0) :
((finset.range n).sum (λ (i : ℕ), polynomial.X ^ i)).monic
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, _⟩)
@[simp]
theorem
polynomial.coeff_restriction
{R : Type u}
[ring R]
{p : polynomial R}
{n : ℕ} :
↑(p.restriction.coeff n) = p.coeff n
@[simp]
theorem
polynomial.coeff_restriction'
{R : Type u}
[ring R]
{p : polynomial R}
{n : ℕ} :
(p.restriction.coeff n).val = 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}
[comm_ring R]
(p : polynomial R) :
polynomial.map (algebra_map ↥(subring.closure ↑(p.frange)) R) p.restriction = p
@[simp]
theorem
polynomial.degree_restriction
{R : Type u}
[ring R]
{p : polynomial R} :
p.restriction.degree = p.degree
@[simp]
@[simp]
theorem
polynomial.monic_restriction
{R : Type u}
[ring R]
{p : polynomial R} :
p.restriction.monic ↔ p.monic
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
noncomputable
def
polynomial.to_subring
{R : Type u}
[ring R]
(p : polynomial R)
(T : subring R)
(hp : ↑(p.frange) ⊆ ↑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, _⟩)
@[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
@[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
@[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
@[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
@[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
@[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
@[simp]
@[simp]
@[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
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))
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)
@[simp]
theorem
polynomial.frange_of_subring
{R : Type u}
[ring R]
(T : subring R)
{p : polynomial ↥T} :
↑((polynomial.of_subring T p).frange) ⊆ ↑T
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
@[simp]
theorem
polynomial.ker_mod_by_monic_hom
{R : Type u}
[comm_ring R]
{q : polynomial R}
(hq : q.monic) :
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].
theorem
ideal.mem_of_polynomial
{R : Type u}
[semiring R]
{I : ideal (polynomial R)}
(x : polynomial R) :
x ∈ I.of_polynomial ↔ x ∈ I
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
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)
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
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
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
theorem
polynomial.ker_map_ring_hom
{R : Type u}
{S : Type u_1}
[comm_semiring R]
[semiring S]
(f : R →+* S) :
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
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
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
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
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 : ℕ) :
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ᵢ.
polynomial R is never a field for any ring R.
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.
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
theorem
ideal.eval₂_C_mk_eq_zero
{R : Type u}
[comm_ring R]
{I : ideal R}
(f : polynomial R)
(H : f ∈ ideal.map polynomial.C I) :
noncomputable
def
ideal.polynomial_quotient_equiv_quotient_polynomial
{R : Type u}
[comm_ring R]
(I : ideal R) :
polynomial (R ⧸ I) ≃+* polynomial R ⧸ 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
- I.polynomial_quotient_equiv_quotient_polynomial = {to_fun := ⇑(polynomial.eval₂_ring_hom (ideal.quotient.lift I ((ideal.quotient.mk (ideal.map polynomial.C I)).comp polynomial.C) ideal.quotient_map_C_eq_zero) (⇑(ideal.quotient.mk (ideal.map polynomial.C I)) polynomial.X)), inv_fun := ⇑(ideal.quotient.lift (ideal.map polynomial.C I) (polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) ideal.eval₂_C_mk_eq_zero), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
theorem
ideal.polynomial_quotient_equiv_quotient_polynomial_symm_mk
{R : Type u}
[comm_ring R]
(I : ideal R)
(f : polynomial R) :
@[simp]
theorem
ideal.polynomial_quotient_equiv_quotient_polynomial_map_mk
{R : Type u}
[comm_ring R]
(I : ideal R)
(f : polynomial R) :
If P is a prime ideal of R, then R[x]/(P) is an integral domain.
theorem
ideal.is_prime_map_C_of_is_prime
{R : Type u}
[comm_ring R]
{P : ideal R}
(H : P.is_prime) :
If P is a prime ideal of R, then P.R[x] is a prime ideal of R[x].
theorem
ideal.eq_zero_of_polynomial_mem_map_range
{R : Type u}
[comm_ring R]
(I : ideal (polynomial R))
(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
theorem
ideal.is_fg_degree_le
{R : Type u}
[comm_ring R]
[is_noetherian_ring R]
(I : ideal (polynomial R))
(n : ℕ) :
theorem
polynomial.prime_C_iff
{R : Type u}
[comm_ring R]
{r : R} :
prime (⇑polynomial.C r) ↔ prime r
theorem
mv_polynomial.prime_C_iff
{R : Type u}
(σ : Type v)
[comm_ring R]
{r : R} :
prime (⇑mv_polynomial.C r) ↔ prime r
theorem
mv_polynomial.prime_rename_iff
{R : Type u}
{σ : Type v}
[comm_ring R]
(s : set σ)
{p : mv_polynomial ↥s R} :
@[protected, instance]
@[protected, instance]
Hilbert basis theorem: a polynomial ring over a noetherian ring is a noetherian ring.
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
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
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
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
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))
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) = ⊤
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))
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))
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)
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)
@[protected, instance]
def
mv_polynomial.is_noetherian_ring
{R : Type u}
{σ : Type v}
[comm_ring R]
[fintype σ]
[is_noetherian_ring R] :
The multivariate polynomial ring in finitely many variables over a noetherian ring is itself a noetherian ring.
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.
theorem
mv_polynomial.no_zero_divisors_of_finite
(R : Type u)
(σ : Type v)
[comm_semiring R]
[finite σ]
[no_zero_divisors 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.
@[protected, instance]
def
mv_polynomial.no_zero_divisors
{R : Type u}
[comm_semiring R]
[no_zero_divisors R]
{σ : Type v} :
@[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.
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
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
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.
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
theorem
mv_polynomial.ker_map
{R : Type u}
{S : Type u_1}
{σ : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S) :
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) :
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
- mv_polynomial.quotient_equiv_quotient_mv_polynomial I = {to_fun := ⇑(mv_polynomial.eval₂_hom (ideal.quotient.lift I ((ideal.quotient.mk (ideal.map mv_polynomial.C I)).comp mv_polynomial.C) _) (λ (i : σ), ⇑(ideal.quotient.mk (ideal.map mv_polynomial.C I)) (mv_polynomial.X i))), inv_fun := ⇑(ideal.quotient.lift (ideal.map mv_polynomial.C I) (mv_polynomial.eval₂_hom (mv_polynomial.C.comp (ideal.quotient.mk I)) mv_polynomial.X) _), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[protected, instance]
def
polynomial.unique_factorization_monoid
{D : Type u}
[comm_ring D]
[is_domain D]
[unique_factorization_monoid D] :
@[protected, instance]
def
mv_polynomial.unique_factorization_monoid
(σ : Type v)
{D : Type u}
[comm_ring D]
[is_domain D]
[unique_factorization_monoid D] :