Polynomial.mem_degreeLT
theorem Polynomial.mem_degreeLT :
∀ {R : Type u} [inst : Semiring R] {n : ℕ} {f : Polynomial R}, f ∈ Polynomial.degreeLT R n ↔ f.degree < ↑n := by
sorry
This theorem states that for any semiring `R`, a natural number `n`, and a polynomial `f` of type `R`, the polynomial `f` is a member of the `R`-submodule of `R[X]` consisting of polynomials of degree less than `n` (denoted as `Polynomial.degreeLT R n`) if and only if the degree of the polynomial `f` (denoted as `Polynomial.degree f`) is less than `n`. Here, the degree of a polynomial is the largest `X`-exponent in the polynomial, or equivalently, the highest power of `X` that appears in the polynomial.
More concisely: For any semiring R, natural number n, and polynomial f over R in one variable X, the polynomial f belongs to the submodule of polynomials of degree less than n if and only if the degree of f is less than n.
|
Polynomial.map_toSubring
theorem Polynomial.map_toSubring :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.frange ⊆ ↑T),
Polynomial.map T.subtype (p.toSubring T hp) = p
The theorem `Polynomial.map_toSubring` states that for any given ring `R`, a polynomial `p` of `R`, and a subring `T` of `R` that contains all the nonzero coefficients of the polynomial `p`, when we map the polynomial created by replacing the coefficients of `p` with their corresponding elements in `T` (using `Polynomial.toSubring`) back to `R` (using `Subring.subtype T`), we get the original polynomial `p`. In more mathematical terms, the theorem shows that the mapping of the polynomial in the subring `T` back to `R` is an identity operation on the set of polynomials whose coefficients are all in `T`.
More concisely: For any ring R, subring T containing all nonzero coefficients of a polynomial p in R, the application of `Polynomial.toSubring p T` followed by `Subring.subtype T` equals p.
|
Polynomial.coeff_prod_mem_ideal_pow_tsub
theorem Polynomial.coeff_prod_mem_ideal_pow_tsub :
∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (f : ι → Polynomial R) (I : Ideal R)
(n : ι → ℕ),
(∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
This theorem states that, in a commutative semiring `R` with an ideal `I`, if we have a finite set of polynomials `pᵢ` each having the property that for all `k`, the `k`-th coefficient `(pᵢ)ₖ` is in `I` raised to the power of `nᵢ-k`, then the product polynomial `p = ∏ pᵢ` also has the property that for all `k`, its `k`-th coefficient `pₖ` is in `I` raised to the power of `∑nᵢ-k`. Here, `nᵢ` and `k` are non-negative integers, and `∑nᵢ` is the sum of all `nᵢ` for each polynomial in the set.
More concisely: If `R` is a commutative semiring with ideal `I`, and each polynomial `pᵢ` in a finite set has coefficients `(pᵢ)ₖ` in `I` raised to the power `nᵢ-k`, then the product polynomial `p` has coefficient `pₖ` in `I` raised to the power `∑nᵢ-k`.
|
MvPolynomial.mem_ideal_of_coeff_mem_ideal
theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal :
∀ {R : Type u} {σ : Type v} [inst : CommRing R] (I : Ideal (MvPolynomial σ R)) (p : MvPolynomial σ R),
(∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p ∈ Ideal.comap MvPolynomial.C I) → p ∈ I
The theorem `MvPolynomial.mem_ideal_of_coeff_mem_ideal` states that, given a commutative ring `R` and a set `σ`, if all coefficients of a multivariate polynomial `p` in `MvPolynomial σ R` are elements of the preimage of an ideal `I` under the constant polynomial map `MvPolynomial.C`, then the polynomial itself is also an element of the ideal `I`. In other words, a multivariate polynomial is in a specific ideal if and only if all of its coefficients are in the preimage of that ideal under the map that assigns each ring element to the corresponding constant polynomial.
More concisely: A multivariate polynomial in `MvPolynomial σ R` lies in ideal `I` if and only if all its coefficients are in the preimage of `I` under the constant polynomial map.
|
Polynomial.isNoetherianRing
theorem Polynomial.isNoetherianRing :
∀ {R : Type u} [inst : CommRing R] [inst_1 : IsNoetherianRing R], IsNoetherianRing (Polynomial R)
The theorem states the Hilbert basis theorem: If a ring 'R' is Noetherian, then the ring of polynomials over 'R' is also Noetherian. A Noetherian ring is one where all its ideals are finitely generated. The theorem generalizes the concept by stating that this property is maintained when we consider the ring of polynomials with coefficients in 'R'.
More concisely: If 'R' is a Noetherian ring, then the polynomial ring 'R[X₁, ..., Xₙ]' over 'R' is also Noetherian.
|
Polynomial.span_le_degreeLE_of_finite
theorem Polynomial.span_le_degreeLE_of_finite :
∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
s.Finite → ∃ n, Submodule.span R s ≤ Polynomial.degreeLE R ↑n
This theorem states that for any semiring `R` and any finite set `s` of polynomials over `R`, there exists a natural number `n` such that the span of `s` (which is the smallest submodule of `R` that contains `s`) is included in (or equal to) the set of polynomials of degree less than or equal to `n` (denoted as `degreeLE n`). In other words, for every finite set of polynomials, all the polynomials that can be formed by linear combinations of the polynomials in the set have degree less than or equal to some fixed natural number.
More concisely: For any semiring `R` and finite set `s` of polynomials over `R`, there exists a natural number `n` such that the span of `s` is contained in the set of polynomials of degree less than or equal to `n`.
|
MvPolynomial.noZeroDivisors_of_finite
theorem MvPolynomial.noZeroDivisors_of_finite :
∀ (R : Type u) (σ : Type v) [inst : CommSemiring R] [inst_1 : Finite σ] [inst_2 : NoZeroDivisors R],
NoZeroDivisors (MvPolynomial σ R)
The theorem `MvPolynomial.noZeroDivisors_of_finite` states that multivariate polynomials in a finite number of variables over a commutative semiring that has no zero divisors itself form an integral domain, meaning that the multivariate polynomials also have no zero divisors. A zero divisor is an element in a ring that can multiply with another non-zero element to give zero. The proof of this fact is constructed by transporting the structure from the theorem `MvPolynomial.noZeroDivisors_fin`. This theorem serves as a stepping stone for proving the general case where there are no finiteness assumptions. To see this general case, refer to the theorem `MvPolynomial.noZeroDivisors`.
More concisely: A multivariate polynomial ring over a commutative semiring without zero divisors is itself an integral domain.
|
Polynomial.span_of_finite_le_degreeLT
theorem Polynomial.span_of_finite_le_degreeLT :
∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
s.Finite → ∃ n, Submodule.span R s ≤ Polynomial.degreeLT R n
This theorem states that for any semiring `R` and any finite set `s` of polynomials over `R`, there exists a natural number `n` such that the span of the set `s` is contained in the submodule of polynomials whose degree is less than `n`. In other words, if you collect a finite number of polynomials and consider the smallest submodule that contains all of them (i.e., the span of `s`), this submodule will always be a subset of the set of all polynomials of degree less than some `n`.
More concisely: For any semiring `R` and finite set `s` of polynomials over `R`, there exists a natural number `n` such that the span of `s` is contained in the submodule of polynomials over `R` of degree less than `n`.
|
Ideal.isPrime_map_C_of_isPrime
theorem Ideal.isPrime_map_C_of_isPrime :
∀ {R : Type u} [inst : CommRing R] {P : Ideal R}, P.IsPrime → (Ideal.map Polynomial.C P).IsPrime
This theorem states that if `P` is a prime ideal in a commutative ring `R`, then the ideal generated by the image of `P` under the map which sends each element of `R` to the constant polynomial with that element as coefficient (denoted `P.R[x]`) is a prime ideal in the ring of polynomials over `R` (`R[x]`). Essentially, the theorem guarantees that mapping a prime ideal through constant polynomials preserves its prime property in the polynomial ring.
More concisely: If `P` is a prime ideal in a commutative ring `R`, then the ideal generated by the images of `P` under the map from `R` to `R[x]` is a prime ideal in `R[x]`.
|
Ideal.polynomial_not_isField
theorem Ideal.polynomial_not_isField : ∀ {R : Type u} [inst : Ring R], ¬IsField (Polynomial R)
This theorem states that for any given ring `R`, the polynomial ring `R[X]` is never a field. In other words, no matter what the ring `R` is, when you consider the set of all polynomials with coefficients in `R`, that set does not form a field.
More concisely: For any ring `R`, the polynomial ring `R[X]` over `R` in the indeterminate `X` is not a field.
|
Polynomial.coeff_restriction
theorem Polynomial.coeff_restriction :
∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {n : ℕ}, ↑(p.restriction.coeff n) = p.coeff n
This theorem states that for any given ring `R`, polynomial `p` of `R`, and natural number `n`, the coefficient at position `n` of the restriction of `p` is equal to the coefficient at position `n` of `p`. Here, the restriction of a polynomial is a new polynomial whose coefficients are in the subring generated by the coefficients of the original polynomial. This theorem essentially asserts that the process of restriction does not affect the coefficients of the polynomial at any given position.
More concisely: For any ring `R`, polynomial `p` over `R`, and natural number `n`, the coefficient of `x^(n)` in the restriction of `p` equals the coefficient of `x^(n)` in `p`.
|
MvPolynomial.mem_map_C_iff
theorem MvPolynomial.mem_map_C_iff :
∀ {R : Type u} {σ : Type v} [inst : CommRing R] {I : Ideal R} {f : MvPolynomial σ R},
f ∈ Ideal.map MvPolynomial.C I ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m f ∈ I
This theorem states that for any commutative ring `R`, any ideal `I` of `R`, and any multi-variable polynomial `f` with coefficients from `R`, `f` is in the push-forward of `I` to the ring of multi-variable polynomials (via the inclusion map) if and only if all coefficients of `f` are in `I`. In the context of the theorem, the push-forward of an ideal refers to the image of the ideal under the map `MvPolynomial.C`, which maps a ring element to a constant polynomial of that value. This theorem essentially characterizes the structure of the push-forward of an ideal in terms of the coefficients of the polynomials.
More concisely: For any commutative ring `R`, ideal `I`, and multi-variable polynomial `f` over `R`, `f` is in the image of `I` under the pushforward map if and only if all coefficients of `f` belong to `I`.
|
MvPolynomial.noZeroDivisors_fin
theorem MvPolynomial.noZeroDivisors_fin :
∀ (R : Type u) [inst : CommSemiring R] [inst_1 : NoZeroDivisors R] (n : ℕ),
NoZeroDivisors (MvPolynomial (Fin n) R)
The theorem `MvPolynomial.noZeroDivisors_fin` states that for any commutative semiring `R` which has no zero divisors (i.e., is an integral domain), and for any natural number `n`, the multivariate polynomials over `R` with variables indexed by `Fin n` (the finite type with `n` elements) also form an integral domain. In other words, there are no zero divisors in the ring of such multivariate polynomials. The proof of this fact is established by induction and used later in proving the general case without any finiteness assumptions, as explained in `MvPolynomial.noZeroDivisors`.
More concisely: The theorem `MvPolynomial.noZeroDivisors_fin` asserts that for any commutative semiring without zero divisors `R`, the multivariate polynomials over `R` with variables indexed by a finite type form an integral domain.
|
Polynomial.coeff_toSubring
theorem Polynomial.coeff_toSubring :
∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (T : Subring R) (hp : ↑p.frange ⊆ ↑T) {n : ℕ},
↑((p.toSubring T hp).coeff n) = p.coeff n
This theorem states that for any ring `R`, any polynomial `p` over `R`, any subring `T` of `R` that contains all the coefficients of `p`, and any natural number `n`, the coefficient of `X^n` in the polynomial obtained by mapping `p` to the subring `T` is equal to the coefficient of `X^n` in `p`. In other words, the process of mapping a polynomial to a subring does not change its coefficients.
More concisely: For any ring `R`, polynomial `p` over `R`, subring `T` of `R` containing `p`'s coefficients, and natural number `n`, the coefficient of `X^n` in the polynomial `p` mapped to `T` equals the coefficient of `X^n` in `p`.
|
Ideal.mem_map_C_iff
theorem Ideal.mem_map_C_iff :
∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {f : Polynomial R},
f ∈ Ideal.map Polynomial.C I ↔ ∀ (n : ℕ), f.coeff n ∈ I
The theorem `Ideal.mem_map_C_iff` states that for any commutative semiring `R`, any ideal `I` of `R`, and any polynomial `f` with coefficients in `R`, the polynomial `f` is in the push-forward of the ideal `I` via the ring homomorphism `Polynomial.C` (which sends each ring element to a constant polynomial with that element as the coefficient) if and only if all the coefficients of `f` are in `I`. In other words, a polynomial belongs to the ideal generated by the image of `I` under the constant polynomial function if and only if every coefficient of that polynomial is an element of the initial ideal `I`.
More concisely: A polynomial belongs to the ideal generated by the constant images of an ideal under the polynomial map if and only if all its coefficients are in the ideal.
|
Ideal.eq_zero_of_constant_mem_of_maximal
theorem Ideal.eq_zero_of_constant_mem_of_maximal :
∀ {R : Type u} [inst : Ring R],
IsField R → ∀ (I : Ideal (Polynomial R)) [hI : I.IsMaximal] (x : R), Polynomial.C x ∈ I → x = 0
This theorem states that if `R` is a field and `I` is a maximal ideal in the ring of polynomials over `R`, then the only constant, `x`, from `R` that can belong to the ideal `I` is `0`. In other words, if a constant polynomial represented by `Polynomial.C x` is in the maximal ideal `I`, then the constant `x` must be `0`.
More concisely: If `I` is a maximal ideal in the polynomial ring over a field `R`, then only the constant `0` belongs to `I` as a constant polynomial.
|
Polynomial.exists_degree_le_of_mem_span
theorem Polynomial.exists_degree_le_of_mem_span :
∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)} {p : Polynomial R},
s.Nonempty → p ∈ Submodule.span R s → ∃ p' ∈ s, p.degree ≤ p'.degree
This theorem states that for any semiring `R` and any set `s` of polynomials over `R`, if `s` is non-empty and a polynomial `p` is in the span of `s` (i.e., `p` can be expressed as a linear combination of polynomials in `s`), then there exists another polynomial `p'` in `s` such that the degree of `p` is less than or equal to the degree of `p'`. This means that within any non-empty set of polynomials, it is always possible to find a polynomial of higher or equal degree to any polynomial in the span of that set.
More concisely: Given a non-empty set `s` of polynomials over a semiring `R`, if a polynomial `p` in their span has degree `d`, then there exists a polynomial `p'` in `s` with degree `d' >= d`.
|
Ideal.polynomial_mem_ideal_of_coeff_mem_ideal
theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal :
∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) (p : Polynomial R),
(∀ (n : ℕ), p.coeff n ∈ Ideal.comap Polynomial.C I) → p ∈ I
This theorem states that if every coefficient of a polynomial `p` belongs to an ideal `I` under the mapping from the coefficient ring to polynomials (using the `Polynomial.C` function), then the polynomial `p` itself is in the ideal `I`. Formally, for any commutative semiring `R`, an ideal `I` of polynomials over `R`, and a polynomial `p` over `R`, if every coefficient of `p` belongs to the preimage of `I` under the constant polynomial map, then `p` belongs to `I`.
More concisely: If every coefficient of a polynomial over a commutative semiring belongs to an ideal under the constant polynomial map, then the polynomial is in the ideal.
|
Ideal.isPrime_map_C_iff_isPrime
theorem Ideal.isPrime_map_C_iff_isPrime :
∀ {R : Type u} [inst : CommRing R] (P : Ideal R), (Ideal.map Polynomial.C P).IsPrime ↔ P.IsPrime
This theorem states that for any commutative ring `R` with a prime ideal `P`, the ideal `P.R[x]` in the polynomial ring `R[x]` is a prime ideal if and only if `P` is a prime ideal in `R`. In other words, the image of a prime ideal under the ring homomorphism that takes coefficients to their corresponding constant polynomials is a prime ideal, if and only if the original ideal was prime.
More concisely: A prime ideal in a commutative ring is mapped to a prime ideal in the polynomial ring over that ring under the homomorphism that takes coefficients to constant polynomials.
|
Polynomial.mem_degreeLE
theorem Polynomial.mem_degreeLE :
∀ {R : Type u} [inst : Semiring R] {n : WithBot ℕ} {f : Polynomial R}, f ∈ Polynomial.degreeLE R n ↔ f.degree ≤ n
This theorem states that for any semiring `R`, any value `n` of type `WithBot ℕ` (which is essentially a natural number that can also be "bottom" or undefined), and any polynomial `f` over `R`, the polynomial `f` is in the `R`-submodule of `R[X]` consisting of polynomials of degree ≤ `n` if and only if the degree of the polynomial `f` is less than or equal to `n`. The degree of a polynomial is defined as the largest exponent in it, or "bottom" if the polynomial is equal to zero.
More concisely: For any semiring R, a polynomial f over R is in the R-submodule of polynomials of degree ≤ n if and only if the degree of f is less than or equal to n.
|
Polynomial.exists_degree_le_of_mem_span_of_finite
theorem Polynomial.exists_degree_le_of_mem_span_of_finite :
∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)},
s.Finite → s.Nonempty → ∃ p' ∈ s, ∀ p ∈ Submodule.span R s, p.degree ≤ p'.degree
This theorem, `Polynomial.exists_degree_le_of_mem_span_of_finite`, states that, for a given semiring `R`, and for a finite and nonempty set `s` of polynomials over `R`, there exists a polynomial `p'` in `s` such that the degree of `p'` is greater than or equal to the degree of any polynomial `p` that is in the span of `s` over `R`. In simpler terms, among all the polynomials that can be generated by linear combinations of the polynomials in `s`, there is at least one polynomial in `s` itself that has a degree as high as, or higher than, any of these generated polynomials.
More concisely: For any semiring `R` and finite, nonempty set `s` of polynomials over `R`, there exists a polynomial `p'` in `s` with the highest degree among polynomials in the span of `s` over `R`.
|
Polynomial.not_finite
theorem Polynomial.not_finite :
∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], ¬Module.Finite R (Polynomial R)
This theorem states that if `R` is a nontrivial ring, then the polynomials `R[X]` cannot be represented as a finite `R`-module. In other words, there is no finite set of polynomials over `R` that can be combined with the ring operations to produce every possible polynomial over `R`. When `R` is a field, this is equivalent to saying that `R[X]` is an infinite-dimensional vector space over `R`, meaning there is no finite basis for `R[X]` over `R`.
More concisely: If `R` is a nontrivial ring, then `R[X]` cannot be finitely generated as an `R`-module.
|
Mathlib.RingTheory.Polynomial.Basic._auxLemma.4
theorem Mathlib.RingTheory.Polynomial.Basic._auxLemma.4 :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, (n ∈ p.support) = (p.coeff n ≠ 0)
This theorem states that for any semiring `R`, any natural number `n`, and any polynomial `p` with coefficients in `R`, the number `n` is in the support of `p` if and only if the coefficient of `X^n` in `p` is non-zero. In other words, the support of a polynomial consists exactly of the exponents of those terms in the polynomial that have a non-zero coefficient.
More concisely: The support of a polynomial `p` in a semiring `R` equals the set of exponents of non-zero coefficients in `p`.
|