# mathlibdocumentation

ring_theory.polynomial.basic

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

def polynomial.degree_le (R : Type u) [comm_ring R] :
(polynomial R)

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

Equations
def polynomial.degree_lt (R : Type u) [comm_ring R] :
(polynomial R)

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

Equations
theorem polynomial.mem_degree_le {R : Type u} [comm_ring R] {n : with_bot } {f : polynomial R} :

theorem polynomial.degree_le_mono {R : Type u} [comm_ring R] {m n : with_bot } :
m n

theorem polynomial.degree_le_eq_span_X_pow {R : Type u} [comm_ring R] {n : } :
= (finset.image (λ (n : ), (finset.range (n + 1)))

theorem polynomial.mem_degree_lt {R : Type u} [comm_ring R] {n : } {f : polynomial R} :

theorem polynomial.degree_lt_mono {R : Type u} [comm_ring R] {m n : } :
m n

theorem polynomial.degree_lt_eq_span_X_pow {R : Type u} [comm_ring R] {n : } :
= (finset.image (λ (n : ), (finset.range n))

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

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

Equations
@[simp]
theorem polynomial.coeff_restriction {R : Type u} [comm_ring R] {p : polynomial R} {n : } :

@[simp]
theorem polynomial.coeff_restriction' {R : Type u} [comm_ring R] {p : polynomial R} {n : } :

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

@[simp]
theorem polynomial.degree_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

@[simp]
theorem polynomial.nat_degree_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

@[simp]
theorem polynomial.monic_restriction {R : Type u} [comm_ring R] {p : polynomial R} :

@[simp]
theorem polynomial.restriction_zero {R : Type u} [comm_ring R] :

@[simp]
theorem polynomial.restriction_one {R : Type u} [comm_ring R] :

theorem polynomial.eval₂_restriction {R : Type u} [comm_ring R] {S : Type v} [ring S] {f : R →+* S} {x : S} {p : polynomial R} :
p = x p.restriction

def polynomial.to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] :
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
@[simp]
theorem polynomial.coeff_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : 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 : 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 : T) :

@[simp]
theorem polynomial.nat_degree_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : T) :

@[simp]
theorem polynomial.monic_to_subring {R : Type u} [comm_ring R] (p : polynomial R) (T : set R) [is_subring T] (hp : T) :

@[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 : T) :
(p.to_subring T hp) = p

def polynomial.of_subring {R : Type u} [comm_ring R] (T : set R) [is_subring T] :

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

Equations
@[simp]
theorem polynomial.frange_of_subring {R : Type u} [comm_ring R] (T : set R) [is_subring T] {p : polynomial T} :

theorem ideal.mem_map_C_iff {R : Type u} [comm_ring R] {I : ideal R} {f : polynomial R} :
∀ (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

theorem ideal.quotient_map_C_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (a : R) :
a I = 0

theorem ideal.eval₂_C_mk_eq_zero {R : Type u} [comm_ring R] {I : ideal R} (f : polynomial R) :

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
def ideal.of_polynomial {R : Type u} [comm_ring R] :

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

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

def ideal.degree_le {R : Type u} [comm_ring R] :
ideal (polynomial R) (polynomial R)

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

Equations
def ideal.leading_coeff_nth {R : Type u} [comm_ring R] :
ideal (polynomial R)

Given an ideal I of R[X], make the ideal in R of leading coefficients of polynomials in I with degree ≤ n.

Equations
theorem ideal.mem_leading_coeff_nth {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : ) (x : R) :
x ∃ (p : (H : p I), p.degree n

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

theorem ideal.leading_coeff_nth_mono {R : Type u} [comm_ring R] (I : ideal (polynomial R)) {m n : } :
m n

def ideal.leading_coeff {R : Type u} [comm_ring R] :
ideal (polynomial R)

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

Equations
theorem ideal.mem_leading_coeff {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (x : R) :
∃ (p : (H : p I),

theorem ideal.is_fg_degree_le {R : Type u} [comm_ring R] (I : ideal (polynomial R)) (n : ) :

@[instance]
theorem polynomial.is_noetherian_ring {R : Type u} [comm_ring 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} {f : polynomial R} :
0 < f.degree(∃ (g : , g f)

theorem polynomial.exists_irreducible_of_nat_degree_pos {R : Type u} {f : polynomial R} :
0 < f.nat_degree(∃ (g : , g f)

theorem polynomial.exists_irreducible_of_nat_degree_ne_zero {R : Type u} {f : polynomial R} :
f.nat_degree 0(∃ (g : , g f)

theorem polynomial.linear_independent_powers_iff_eval₂ {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) (v : M) :
(λ (n : ), (f ^ n) v) ∀ (p : , ( p) v = 0p = 0

theorem polynomial.disjoint_ker_aeval_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} :
qdisjoint ( p).ker ( q).ker

theorem polynomial.sup_aeval_range_eq_top_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} :
q( p).range ( q).range =

theorem polynomial.sup_ker_aeval_le_ker_aeval_mul {R : Type u} {M : Type w} [comm_ring R] [ M] {f : M →ₗ[R] M} {p q : polynomial R} :
( p).ker ( q).ker ( (p * q)).ker

theorem polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime {R : Type u} {M : Type w} [comm_ring R] [ M] (f : M →ₗ[R] M) {p q : polynomial R} :
q( p).ker ( q).ker = ( (p * q)).ker

@[instance]
def mv_polynomial.is_noetherian_ring {R : Type u} {σ : Type v} [comm_ring R] [fintype σ]  :

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

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) [fintype σ] :

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} {σ : Type v} (p q : R) :
p * q = 0p = 0 q = 0

@[instance]
def mv_polynomial.integral_domain {R : Type u} {σ : Type v}  :

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

Equations