@[instance]
The R-submodule of R[X] consisting of polynomials of degree ≤ n.
Equations
- polynomial.degree_le R n = ⨅ (k : ℕ) (h : ↑k > n), (polynomial.lcoeff R k).ker
The R-submodule of R[X] consisting of polynomials of degree < n.
Equations
- polynomial.degree_lt R n = ⨅ (k : ℕ) (h : k ≥ n), (polynomial.lcoeff R k).ker
theorem
polynomial.mem_degree_le
{R : Type u}
[comm_ring R]
{n : with_bot ℕ}
{f : polynomial R} :
f ∈ polynomial.degree_le R n ↔ f.degree ≤ n
theorem
polynomial.degree_le_mono
{R : Type u}
[comm_ring R]
{m n : with_bot ℕ} :
m ≤ n → polynomial.degree_le R m ≤ polynomial.degree_le R n
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)))
theorem
polynomial.degree_lt_mono
{R : Type u}
[comm_ring R]
{m n : ℕ} :
m ≤ n → polynomial.degree_lt R m ≤ polynomial.degree_lt R n
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))
Given a polynomial, return the polynomial whose coefficients are in the ring closure of the original coefficients.
Equations
- p.restriction = {support := p.support, to_fun := λ (i : ℕ), ⟨p.to_fun i, _⟩, mem_support_to_fun := _}
@[simp]
theorem
polynomial.coeff_restriction
{R : Type u}
[comm_ring R]
{p : polynomial R}
{n : ℕ} :
↑(p.restriction.coeff n) = p.coeff n
@[simp]
theorem
polynomial.coeff_restriction'
{R : Type u}
[comm_ring R]
{p : polynomial R}
{n : ℕ} :
(p.restriction.coeff n).val = p.coeff n
@[simp]
theorem
polynomial.map_restriction
{R : Type u}
[comm_ring R]
(p : polynomial R) :
polynomial.map (algebra_map ↥(ring.closure ↑(finsupp.frange p)) R) p.restriction = p
@[simp]
theorem
polynomial.degree_restriction
{R : Type u}
[comm_ring R]
{p : polynomial R} :
p.restriction.degree = p.degree
@[simp]
@[simp]
theorem
polynomial.monic_restriction
{R : Type u}
[comm_ring R]
{p : polynomial R} :
p.restriction.monic ↔ p.monic
theorem
polynomial.eval₂_restriction
{R : Type u}
[comm_ring R]
{S : Type v}
[ring S]
{f : R →+* S}
{x : S}
{p : polynomial R} :
polynomial.eval₂ f x p = polynomial.eval₂ (f.comp (is_subring.subtype (ring.closure ↑(finsupp.frange p)))) x p.restriction
def
polynomial.to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T] :
↑(finsupp.frange p) ⊆ 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 = {support := p.support, to_fun := λ (i : ℕ), ⟨p.to_fun i, _⟩, mem_support_to_fun := _}
@[simp]
theorem
polynomial.coeff_to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T)
{n : ℕ} :
↑((p.to_subring T hp).coeff n) = p.coeff n
@[simp]
theorem
polynomial.coeff_to_subring'
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T)
{n : ℕ} :
((p.to_subring T hp).coeff n).val = p.coeff n
@[simp]
theorem
polynomial.degree_to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T) :
(p.to_subring T hp).degree = p.degree
@[simp]
theorem
polynomial.nat_degree_to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T) :
(p.to_subring T hp).nat_degree = p.nat_degree
@[simp]
theorem
polynomial.monic_to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T) :
(p.to_subring T hp).monic ↔ p.monic
@[simp]
theorem
polynomial.to_subring_zero
{R : Type u}
[comm_ring R]
(T : set R)
[is_subring T] :
0.to_subring T _ = 0
@[simp]
theorem
polynomial.to_subring_one
{R : Type u}
[comm_ring R]
(T : set R)
[is_subring T] :
1.to_subring T _ = 1
@[simp]
theorem
polynomial.map_to_subring
{R : Type u}
[comm_ring R]
(p : polynomial R)
(T : set R)
[is_subring T]
(hp : ↑(finsupp.frange p) ⊆ T) :
polynomial.map (is_subring.subtype T) (p.to_subring T hp) = p
def
polynomial.of_subring
{R : Type u}
[comm_ring R]
(T : set R)
[is_subring T] :
polynomial ↥T → polynomial R
Given a polynomial whose coefficients are in some subring, return the corresponding polynomial whose coefificents are in the ambient ring.
Equations
- polynomial.of_subring T p = {support := p.support, to_fun := subtype.val ∘ p.to_fun, mem_support_to_fun := _}
@[simp]
theorem
polynomial.frange_of_subring
{R : Type u}
[comm_ring R]
(T : set R)
[is_subring T]
{p : polynomial ↥T} :
↑(finsupp.frange (polynomial.of_subring T p)) ⊆ T
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
ideal.quotient_map_C_eq_zero
{R : Type u}
[comm_ring R]
{I : ideal R}
(a : R) :
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) :
f ∈ ideal.map polynomial.C I → ⇑(polynomial.eval₂_ring_hom (polynomial.C.comp (ideal.quotient.mk I)) polynomial.X) f = 0
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
- ideal.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' := _}
def
ideal.of_polynomial
{R : Type u}
[comm_ring R] :
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}
[comm_ring R]
{I : ideal (polynomial R)}
(x : polynomial R) :
x ∈ I.of_polynomial ↔ x ∈ I
def
ideal.degree_le
{R : Type u}
[comm_ring R] :
ideal (polynomial R) → 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
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)
theorem
ideal.mem_leading_coeff_nth
{R : Type u}
[comm_ring 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_ring 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_ring R]
(I : ideal (polynomial R))
{m n : ℕ} :
m ≤ n → I.leading_coeff_nth m ≤ I.leading_coeff_nth n
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.mem_leading_coeff
{R : Type u}
[comm_ring R]
(I : ideal (polynomial R))
(x : R) :
x ∈ I.leading_coeff ↔ ∃ (p : polynomial R) (H : p ∈ I), p.leading_coeff = x
theorem
ideal.is_fg_degree_le
{R : Type u}
[comm_ring R]
(I : ideal (polynomial R))
[is_noetherian_ring R]
(n : ℕ) :
@[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}
[integral_domain R]
[is_noetherian_ring R]
{f : polynomial R} :
0 < f.degree → (∃ (g : polynomial R), irreducible g ∧ g ∣ f)
theorem
polynomial.exists_irreducible_of_nat_degree_pos
{R : Type u}
[integral_domain R]
[is_noetherian_ring R]
{f : polynomial R} :
0 < f.nat_degree → (∃ (g : polynomial R), irreducible g ∧ g ∣ f)
theorem
polynomial.exists_irreducible_of_nat_degree_ne_zero
{R : Type u}
[integral_domain R]
[is_noetherian_ring R]
{f : polynomial R} :
f.nat_degree ≠ 0 → (∃ (g : polynomial R), irreducible g ∧ g ∣ f)
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)
@[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.
Equations
theorem
mv_polynomial.is_integral_domain_fin_zero
(R : Type u)
[comm_ring R] :
is_integral_domain R → is_integral_domain (mv_polynomial (fin 0) R)
theorem
mv_polynomial.is_integral_domain_fin
(R : Type u)
[comm_ring R]
(hR : is_integral_domain R)
(n : ℕ) :
is_integral_domain (mv_polynomial (fin n) R)
Auxilliary 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.integral_domain for the general case.
theorem
mv_polynomial.is_integral_domain_fintype
(R : Type u)
(σ : Type v)
[comm_ring R]
[fintype σ] :
def
mv_polynomial.integral_domain_fintype
(R : Type u)
(σ : Type v)
[integral_domain R]
[fintype σ] :
integral_domain (mv_polynomial σ R)
Auxilliary 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.integral_domain_fin,
and then used to prove the general case without finiteness hypotheses.
See mv_polynomial.integral_domain for the general case.
Equations
theorem
mv_polynomial.eq_zero_or_eq_zero_of_mul_eq_zero
{R : Type u}
[integral_domain R]
{σ : Type v}
(p q : mv_polynomial σ R) :
@[instance]
def
mv_polynomial.integral_domain
{R : Type u}
{σ : Type v}
[integral_domain R] :
integral_domain (mv_polynomial σ R)
The multivariate polynomial ring over an integral domain is an integral domain.
Equations
- mv_polynomial.integral_domain = {add := comm_ring.add mv_polynomial.comm_ring, add_assoc := _, zero := comm_ring.zero mv_polynomial.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg mv_polynomial.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul mv_polynomial.comm_ring, mul_assoc := _, one := comm_ring.one mv_polynomial.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}