LeanAide documentation

LeanAide GPT-4 documentation

Module: Mathlib.Algebra.Polynomial.Degree.Definitions

`Polynomial.sum_over_range'` theorem Polynomial.sum_over_range' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S}, (∀ (n : ℕ), f n 0 = 0) → ∀ (n : ℕ), p.natDegree < n → p.sum f = (Finset.range n).sum fun a => f a (p.coeff a) This theorem states that for any polynomial `p` over a semiring `R` and any function `f` from pairs of natural numbers and elements of `R` to an additive commutative monoid `S` that maps any pair `(n, 0)` to `0`, there exists a natural number `n` larger than the natural degree of `p` such that the sum of `f` applied to the coefficients of `p` is equal to the sum of `f` applied to the coefficients of `p` for each natural number less than `n`. This allows us to recast the sum over `p.support` (the nonzero coefficients of the polynomial) as a sum over the range of natural numbers less than `n`. More concisely: For any polynomial `p` over a semiring `R` and additive commutative monoid homomorphism `f` mapping `(n, 0)` to `0`, there exists a natural number `n` greater than the degree of `p` such that the sum of `f` applied to `p`'s coefficients equals the sum over coefficients with index less than `n`.
`Polynomial.Monic.coeff_natDegree` theorem Polynomial.Monic.coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.coeff p.natDegree = 1 The theorem `Polynomial.Monic.coeff_natDegree` states that for all types `R` that have a semiring structure and for all polynomials `p` over `R`, if `p` is a monic polynomial (i.e., its leading coefficient is 1), then the coefficient of `p` at the degree of `p` forced to a natural number (`natDegree p`) is also 1. In other words, it asserts that the coefficient of the highest non-zero degree term (in natural numbers) of a monic polynomial is 1. More concisely: For every monic polynomial $p$ over a semiring $R$, the coefficient of $p$ at its natural degree is 1.
`Polynomial.natDegree_neg` theorem Polynomial.natDegree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).natDegree = p.natDegree := by sorry The theorem `Polynomial.natDegree_neg` states that for any type `R` equipped with a ring structure, and for any polynomial `p` of type `R`, the natural degree of the negation of `p` (`-p`) is equal to the natural degree of `p`. In other words, negating a polynomial does not change its natural degree. More concisely: The natural degree of the negation of a polynomial is equal to the natural degree of the polynomial in any commutative ring.
`Polynomial.leadingCoeff_X_add_C` theorem Polynomial.leadingCoeff_X_add_C : ∀ {S : Type v} [inst : Semiring S] (r : S), (Polynomial.X + Polynomial.C r).leadingCoeff = 1 The theorem `Polynomial.leadingCoeff_X_add_C` states that for any type `S` that forms a semiring and for any element `r` belonging to `S`, the leading coefficient of the polynomial which is the sum of the polynomial variable `X` and the constant polynomial `r` is always 1. This means that the highest degree term in the polynomial `X + r` (where `r` is a constant) always has the coefficient 1. More concisely: The leading coefficient of the polynomial `X + r` in a semiring is always 1, where `X` is a polynomial variable and `r` is a constant.
`Polynomial.leadingCoeff_monic_mul` theorem Polynomial.leadingCoeff_monic_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → (p * q).leadingCoeff = q.leadingCoeff This theorem states that for any semiring `R` and any polynomials `p` and `q` from `R`, if the polynomial `p` is monic (i.e., its leading coefficient is 1), then the leading coefficient of the polynomial obtained by multiplying `p` and `q` is the same as the leading coefficient of `q` itself. More concisely: For any semiring `R` and monic polynomials `p` and `q` from `R`, the leading coefficient of their product `p q` equals the leading coefficient of `q`.*
`Polynomial.natDegree_X_pow` theorem Polynomial.natDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ), (Polynomial.X ^ n).natDegree = n This theorem states that for any natural number `n`, the natural degree of the `n`-th power of the polynomial variable `X` (commonly known as the indeterminate) is equal to `n` itself. This fact holds for any semiring `R` that is nontrivial. In other words, it asserts that the degree (as a natural number) of the polynomial `X^n` is `n`, where `X` is the polynomial variable in the semiring `R`. More concisely: For any natural number `n` and semiring `R`, the degree of the `n`-th power of the polynomial variable `X` in `R` is `n`.
`Polynomial.degree_add_le_of_degree_le` theorem Polynomial.degree_add_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, p.degree ≤ ↑n → q.degree ≤ ↑n → (p + q).degree ≤ ↑n The theorem `Polynomial.degree_add_le_of_degree_le` states that for any semiring `R`, and any polynomials `p` and `q` over `R`, and any natural number `n`, if the degree of `p` is less than or equal to `n`, and the degree of `q` is also less than or equal to `n`, then the degree of the polynomial resulting from adding `p` and `q` is also less than or equal to `n`. In other words, the theorem confirms that the degree of the sum of two polynomials will not exceed the maximum degree of the two original polynomials, given that their degrees are both bounded by a certain natural number. More concisely: For any semiring R and polynomials p and q over R of degrees less than or equal to natural number n, the degree of p + q is less than or equal to n.
`Polynomial.leadingCoeff_ne_zero` theorem Polynomial.leadingCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff ≠ 0 ↔ p ≠ 0 The theorem `Polynomial.leadingCoeff_ne_zero` states that for any semiring `R` and any polynomial `p` with coefficients in `R`, the leading coefficient of `p` is not zero if and only if the polynomial `p` is not the zero polynomial. Here, the leading coefficient of a polynomial is defined as the coefficient of the highest power of `X` in the polynomial. More concisely: For any semiring R and polynomial p with coefficients in R, the leading coefficient of p is non-zero if and only if p is not the zero polynomial.
`Polynomial.natDegree_mul_le` theorem Polynomial.natDegree_mul_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p * q).natDegree ≤ p.natDegree + q.natDegree This theorem states that for any semiring `R` and any two polynomials `p` and `q` over `R`, the natural degree of the product of `p` and `q` is less than or equal to the sum of the natural degrees of `p` and `q`. In mathematical terms, if $p$ and $q$ are polynomials over a semiring, then the degree of $p \times q$ is less than or equal to the degree of $p$ plus the degree of $q$. More concisely: The natural degree of the product of two polynomials over a semiring does not exceed the sum of their degrees.
`Polynomial.natDegree_add_eq_left_of_natDegree_lt` theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.natDegree < p.natDegree → (p + q).natDegree = p.natDegree This theorem states that for any semiring `R`, and any two polynomials `p` and `q` over `R`, if the natural degree of `q` is less than the natural degree of `p`, then the natural degree of the sum of `p` and `q` is equal to the natural degree of `p`. In terms of algebra, the degree of a polynomial is the highest power of its variable. So in essence, when adding two polynomials, if one polynomial (`q`) has a degree less than the other (`p`), the degree of the resulting polynomial is equal to the degree of the polynomial with the higher degree. More concisely: Given two polynomials `p` and `q` over a semiring `R` with the natural degree of `q` strictly less than that of `p`, the natural degree of `p + q` equals the natural degree of `p`.
`Polynomial.natDegree_pow_le` theorem Polynomial.natDegree_pow_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (p ^ n).natDegree ≤ n * p.natDegree The theorem `Polynomial.natDegree_pow_le` states that for any type `R` that is a semiring, for any polynomial `p` of type `R`, and for any natural number `n`, the natural degree of the polynomial `p` raised to the power of `n` is less than or equal to `n` times the natural degree of `p`. In mathematical terms, if we denote the natural degree of a polynomial `p` as `deg(p)`, this theorem asserts that `deg(p^n) ≤ n * deg(p)` for any `n` in natural numbers. More concisely: For any semiring R and polynomial p of type R, the natural degree of p raised to the power n is less than or equal to n times the natural degree of p. Equivalently, deg(p^n) ≤ n * deg(p) for all natural numbers n.
`Polynomial.degree_mul` theorem Polynomial.degree_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R}, (p * q).degree = p.degree + q.degree The theorem `Polynomial.degree_mul` states that for any type `R` that is a semiring and has no zero divisors, and for any polynomials `p` and `q` over `R`, the degree of the product of `p` and `q` is equal to the sum of the degrees of `p` and `q`. In other words, it mathematically represents the property that the degree of the product of two polynomials is the sum of their degrees, i.e. if $p(x)$ and $q(x)$ are two polynomials, then $\deg(p(x)q(x)) = \deg(p(x)) + \deg(q(x))$. More concisely: For polynomials $p$ and $q$ over a semiring $R$ without zero divisors, the degree of their product is equal to the sum of their degrees.
`Polynomial.natDegree_X` theorem Polynomial.natDegree_X : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.X.natDegree = 1 This theorem states that for any type `R` that is equipped with a semiring structure and the property of non-triviality (meaning that there is at least one element in `R` that is not the additive identity), the natural degree of the monomial polynomial `X` (which is the polynomial variable or indeterminate) is `1`. In mathematical terms, it is saying that the degree of the polynomial `X` is `1` in any nontrivial semiring. More concisely: In any semiring endowed with non-triviality, the degree of the monomial polynomial X is 1.
`Polynomial.natDegree_X_pow_add_C` theorem Polynomial.natDegree_X_pow_add_C : ∀ {R : Type u} [inst : Nontrivial R] [inst : Semiring R] {n : ℕ} {r : R}, (Polynomial.X ^ n + Polynomial.C r).natDegree = n The theorem `Polynomial.natDegree_X_pow_add_C` states that for any non-trivial semiring `R`, for any natural number `n` and any element `r` from `R`, the natural degree of the polynomial that is the sum of the polynomial `X` raised to the power `n` and the constant polynomial `r` is equal to `n`. In other words, the degree of a polynomial formed by adding a constant to a monomial is determined solely by the degree of the monomial. More concisely: The natural degree of a polynomial equal to `X^n + constant` in a semiring is `n`, where `n` is a natural number and `constant` is an element from the semiring.
`Polynomial.nextCoeff_of_natDegree_pos` theorem Polynomial.nextCoeff_of_natDegree_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree → p.nextCoeff = p.coeff (p.natDegree - 1) The theorem `Polynomial.nextCoeff_of_natDegree_pos` states that for any semiring `R` and any polynomial `p` over `R`, if the natural degree of `p` is greater than zero, then the next coefficient of `p` is equal to the coefficient of `p` at the position of its natural degree minus one. In other words, for a non-zero-degree polynomial, its next coefficient is simply the coefficient of the term with one degree less. This theorem bridges the relation between the next coefficient and the natural degree of the polynomial in a semiring. More concisely: For any semiring `R` and polynomial `p` of positive degree over `R`, the next coefficient of `p` is equal to the coefficient of `p` at degree `n-1`, where `n` is the degree of `p`.
`Polynomial.natDegree_of_subsingleton` theorem Polynomial.natDegree_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [inst_1 : Subsingleton R], p.natDegree = 0 The theorem `Polynomial.natDegree_of_subsingleton` states that for any type `R` with a `Semiring` structure, if `R` is a subsingleton (i.e., it has at most one element), then the natural degree of any polynomial `p` with coefficients in `R` is 0. In effect, this theorem shows that in a context where the ring of coefficients only contains one element (like the trivial ring), all polynomials are considered as having a degree of 0. More concisely: If a type `R` equipped with a `Semiring` structure is a subsingleton, then the natural degree of any polynomial over `R` is 0.
`Polynomial.leadingCoeff_C` theorem Polynomial.leadingCoeff_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).leadingCoeff = a := by sorry The theorem `Polynomial.leadingCoeff_C` states that for any type `R` equipped with a semiring structure and any element `a` of `R`, the leading coefficient of the constant polynomial `a` is `a` itself. In other words, if we create a polynomial that is a constant `a`, the coefficient of the highest-powered `X` term in this polynomial is `a`. This is true regardless of what `R` or `a` are, so long as `R` is a semiring. More concisely: For any semiring `R` and constant polynomial `a` in `R[X]`, the leading coefficient of `a` is equal to `a`.
`Polynomial.degree_le_iff_coeff_zero` theorem Polynomial.degree_le_iff_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (n : WithBot ℕ), f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0 The theorem `Polynomial.degree_le_iff_coeff_zero` states that for any polynomial `f` over a semiring `R`, and any natural number `n` possibly extended with the bottom element `⊥`, the degree of `f` is less than or equal to `n` if and only if the coefficients of `f` for all powers `m` greater than `n` are zero. In other words, the degree of a polynomial is determined by the highest exponent with a non-zero coefficient. More concisely: The degree of a polynomial over a semiring is less than or equal to a given natural number if and only if all its coefficients for powers greater than that number are zero.
`Polynomial.natDegree_C_mul_X_pow` theorem Polynomial.natDegree_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).natDegree = n := by sorry The theorem `Polynomial.natDegree_C_mul_X_pow` states that for any semiring `R`, any natural number `n`, and any element `a` of this semiring `R` that is not zero, the natural degree of the polynomial obtained by multiplying the constant polynomial `a` and the polynomial variable `X` raised to the power `n` is `n`. In other words, the degree of a non-zero constant times a variable raised to a certain power is equal to that power within the context of polynomial mathematics. More concisely: For any semiring R, natural number n, and non-zero element a in R, the degree of the polynomial a X^n is n.*
`Polynomial.natDegree_X_pow_sub_C` theorem Polynomial.natDegree_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] {n : ℕ} {r : R}, (Polynomial.X ^ n - Polynomial.C r).natDegree = n The theorem `Polynomial.natDegree_X_pow_sub_C` states that for any ring `R` which is nontrivial, and for any natural number `n` and any element `r` of `R`, the degree of the polynomial (when forced to ℕ) resulting from the subtraction of the constant polynomial `r` from the polynomial `X^n` (which is the variable polynomial `X` raised to the power `n`) equals `n`. This essentially means that the degree of the polynomial `X^n - r` is `n`. More concisely: For any nontrivial ring R and natural number n, the degree of X^n - r is n.
`Polynomial.degree_smul_le` theorem Polynomial.degree_smul_le : ∀ {R : Type u} [inst : Semiring R] (a : R) (p : Polynomial R), (a • p).degree ≤ p.degree The theorem `Polynomial.degree_smul_le` states that for any semiring `R`, for any element `a` of `R`, and for any polynomial `p` over `R`, the degree of the polynomial resulting from the scalar multiplication of `p` by `a`, denoted as `a • p`, is less than or equal to the degree of the original polynomial `p`. In other words, scaling a polynomial by a scalar does not increase its degree. More concisely: For any semiring R, element a of R, and polynomial p over R, the degree of a • p is less than or equal to the degree of p.
`Polynomial.degree_X` theorem Polynomial.degree_X : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.X.degree = 1 := by sorry The theorem `Polynomial.degree_X` states that for any instance of a semiring `R` that is nontrivial, the degree of the polynomial `Polynomial.X` is `1`. In this context, `Polynomial.X` is a polynomial variable and the degree of a polynomial is the highest power of the variable that appears in the polynomial. Thus, this theorem is essentially saying that the degree of the polynomial variable itself is `1`, which is consistent with the notion that `Polynomial.X` represents a polynomial of the form `x^1`. More concisely: For any nontrivial semiring R, the degree of the polynomial variable Polynomial.X is 1.
`Polynomial.natDegree_eq_zero_iff_degree_le_zero` theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 ↔ p.degree ≤ 0 This theorem states that for any type `R` that is a semiring and for any polynomial `p` over `R`, the natural degree of `p` is zero if and only if the degree of `p` is less than or equal to zero. The natural degree of a polynomial is the largest exponent of 'X' that appears in the polynomial, with the special case that the natural degree of the zero polynomial is zero. The degree of a polynomial is similar, but it returns a bottom type (`⊥`) for the zero polynomial, meaning it's undefined or not applicable. This theorem connects these two definitions. More concisely: For any semiring `R` and polynomial `p` over `R`, the natural degree and degree of `p` are equal when `p` is not the zero polynomial.
`Polynomial.zero_le_degree_iff` theorem Polynomial.zero_le_degree_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 ≤ p.degree ↔ p ≠ 0 This theorem states that for any given type `R` with a semiring structure and any polynomial `p` of type `R`, the degree of the polynomial `p` is greater than or equal to zero if and only if the polynomial `p` is not equal to zero. In other words, a polynomial has a non-negative degree if it is non-zero; conversely, if a polynomial has a non-negative degree, it must be non-zero. More concisely: A polynomial over a semiring is non-zero if and only if it has non-negative degree.
`Polynomial.le_natDegree_of_mem_supp` theorem Polynomial.le_natDegree_of_mem_supp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ∀ a ∈ p.support, a ≤ p.natDegree The theorem `Polynomial.le_natDegree_of_mem_supp` states that for any type `R` that is a semiring and any polynomial `p` of that type, if a natural number `a` is in the support of `p` (that is, the coefficient of `X^a` in `p` is non-zero), then `a` is less than or equal to the natural degree of `p`. In other words, the degree of a polynomial is at least as large as any exponent of `X` whose coefficient is non-zero. More concisely: For any semiring type R and polynomial p of type R[X], if a is a natural number in the support of p, then a <= degree p.
`Polynomial.eq_C_of_degree_le_zero` theorem Polynomial.eq_C_of_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 0 → p = Polynomial.C (p.coeff 0) This theorem states that for any polynomial `p` over a semiring `R`, if the degree of `p` is less than or equal to 0, then `p` is equal to the constant polynomial `C` with the coefficient of `p` at 0. In other words, if a polynomial has no terms of degree higher than zero, then it is a constant polynomial, and its value is equal to its coefficient at 0. More concisely: For any polynomial `p` over a semiring `R` of degree zero or less, `p` equals the constant polynomial with coefficient `p.0`.
`Polynomial.as_sum_range` theorem Polynomial.as_sum_range : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = (Finset.range (p.natDegree + 1)).sum fun i => (Polynomial.monomial i) (p.coeff i) The theorem `Polynomial.as_sum_range` states that for any polynomial `p` over a semiring `R`, `p` can be expressed as the sum of its monomials, where each monomial `aX^i` is obtained by multiplying the coefficient of `X^i` in `p` by `X^i` (obtained using the `Polynomial.monomial` function), and the sum ranges over all natural numbers `i` from `0` to the degree of `p` (obtained using `Polynomial.natDegree` function). This is the formalization of the standard representation of a polynomial as a sum of monomials. More concisely: For any polynomial `p` over a semiring `R`, `p` can be expressed as the sum of monomials `aX^i` with coefficients `a` taken from `R` and indices `i` ranging from `0` to the degree of `p`.
`Polynomial.natDegree_X_add_C` theorem Polynomial.natDegree_X_add_C : ∀ {R : Type u} [inst : Nontrivial R] [inst : Semiring R] (x : R), (Polynomial.X + Polynomial.C x).natDegree = 1 This theorem states that for any type `R` that is a nontrivial semiring, and for any element `x` of `R`, the natural degree of the polynomial which is the sum of the polynomial variable `X` and the constant polynomial `C x` is always `1`. This means that the polynomial `X + C x` is treated as a first-degree polynomial regardless of the value of `x` in the semiring `R`. More concisely: For any nontrivial semiring `R` and its element `x`, the polynomial `X + C x` has degree 1.
`Polynomial.eq_C_of_natDegree_eq_zero` theorem Polynomial.eq_C_of_natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 → p = Polynomial.C (p.coeff 0) This theorem states that for any polynomial `p` of type `R`, where `R` is a semiring, if the natural degree of `p` is zero, then `p` is equal to the constant polynomial `C` with the coefficient of `p` at zero. In mathematical terms, if a polynomial has a degree of zero, then it is a constant polynomial, with the constant being the coefficient of the polynomial at zero. More concisely: For any polynomial `p` over a semiring `R` of degree zero, `p` equals the constant polynomial `C` with coefficient `p.0`.
`Polynomial.leadingCoeff_mul'` theorem Polynomial.leadingCoeff_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff The theorem `Polynomial.leadingCoeff_mul'` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the product of the leading coefficients of `p` and `q` is nonzero, then the leading coefficient of the product polynomial `p * q` is equal to the product of the leading coefficients of `p` and `q`. In other words, if neither of the polynomials `p` and `q` is the zero polynomial (as indicated by their leading coefficients being nonzero), then when we multiply these two polynomials, the leading coefficient of the resulting polynomial will be the product of the leading coefficients of `p` and `q`. More concisely: If `R` is a semiring and `p` and `q` are polynomials over `R` with nonzero leading coefficients, then the leading coefficient of `p * q` is equal to the product of the leading coefficients of `p` and `q`.
`Polynomial.degree_C_le` theorem Polynomial.degree_C_le : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).degree ≤ 0 This theorem states that for any semiring `R` and any element `a` from `R`, the degree of the constant polynomial `C a` is less than or equal to zero. In other words, the highest power of `X` that appears in the constant polynomial is zero or, in a case where the constant is zero, there are no terms at all. This is based on our definition where the degree of a polynomial is the highest power of `X` that appears in the polynomial, and the degree of the zero polynomial is negative infinity (`⊥`). More concisely: For any semiring `R` and its element `a`, the degree of the constant polynomial `C a` (where `C` is the constant polynomial functor) is less than or equal to zero.
`Polynomial.degree_linear_le` theorem Polynomial.degree_linear_le : ∀ {R : Type u} {a b : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1 := by sorry The theorem `Polynomial.degree_linear_le` states that for any semiring `R` and any elements `a` and `b` of `R`, the degree of the polynomial `(Polynomial.C a * Polynomial.X + Polynomial.C b)`, which is essentially a linear polynomial `ax + b`, is less than or equal to 1. Here, `Polynomial.C a` is the constant polynomial `a`, `Polynomial.X` is the polynomial variable (the equivalent of `x` in mathematical notation), and `Polynomial.degree` computes the highest power of the polynomial variable that appears in the polynomial. More concisely: The degree of the linear polynomial `ax + b` over a semiring is less than or equal to 1, where `a` and `b` are elements of the semiring and `x` is the polynomial variable.
`Polynomial.eq_C_of_degree_eq_zero` theorem Polynomial.eq_C_of_degree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree = 0 → p = Polynomial.C (p.coeff 0) The theorem `Polynomial.eq_C_of_degree_eq_zero` states that for any semiring `R` and any polynomial `p` over `R`, if the degree of `p` is zero, then `p` is equal to the constant polynomial `C` with coefficient equal to the coefficient of `X^0` in `p`. In other words, if the degree of a polynomial is zero, this polynomial is just a constant term, which is the coefficient of `X^0`. More concisely: For any semiring `R` and polynomial `p` over `R` of degree zero, `p` equals the constant polynomial with coefficient equal to `p.coeff 0`.
`Polynomial.Monic.leadingCoeff` theorem Polynomial.Monic.leadingCoeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.leadingCoeff = 1 The theorem `Polynomial.Monic.leadingCoeff` states that for any semiring `R` and any polynomial `p` over `R`, if `p` is monic (that is, its leading coefficient is 1), then the leading coefficient of `p` equals 1. In other words, for a monic polynomial, the coefficient of the term of the polynomial with the highest power of `X` is always 1. More concisely: If `p` is a monic polynomial over semiring `R`, then the leading coefficient of `p` is equal to 1.
`Polynomial.natDegree_lt_natDegree_iff` theorem Polynomial.natDegree_lt_natDegree_iff : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p ≠ 0 → (p.natDegree < q.natDegree ↔ p.degree < q.degree) This theorem states that, for any type `R` that is a semiring and any two polynomials `p` and `q` over `R`, if `p` is not the zero polynomial, then the natural degree of `p` is less than the natural degree of `q` if and only if the degree of `p` is less than the degree of `q`. The natural degree of a polynomial is the highest power of `X` that appears in the polynomial, with the natural degree of the zero polynomial defined as 0. The degree of a polynomial is similar to the natural degree, but it is allowed to be bottom (⊥), which is the case for the zero polynomial. More concisely: For any semiring type `R`, if non-zero polynomials `p` and `q` over `R` have different degrees, then their natural degrees are strictly less than or equal to their respective degrees.
`Polynomial.leadingCoeff_zero` theorem Polynomial.leadingCoeff_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.leadingCoeff 0 = 0 The theorem `Polynomial.leadingCoeff_zero` states that for any type `R` that forms a semiring, the leading coefficient of the zero polynomial is zero. Here, the leading coefficient of a polynomial is defined as the coefficient of the term with the highest power of `X`. In other words, if we have a polynomial which is identically zero, then the coefficient of its highest degree term (which doesn't exist because all terms are zero) is also zero. More concisely: For any semiring `R`, the leading coefficient of the zero polynomial is 0.
`Polynomial.leadingCoeff_X_pow` theorem Polynomial.leadingCoeff_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).leadingCoeff = 1 The theorem `Polynomial.leadingCoeff_X_pow` states that for any semiring `R` and any natural number `n`, the leading coefficient of the polynomial `X` raised to the power `n` is `1`. Here, `X` is the polynomial variable, and the leading coefficient of a polynomial is the coefficient of the term with the highest degree. Hence, regardless of the power `n`, the leading coefficient is always `1` for `X^n`. More concisely: For any semiring R, the leading coefficient of the polynomial X raised to the power n is 1.
`Polynomial.coeff_eq_zero_of_degree_lt` theorem Polynomial.coeff_eq_zero_of_degree_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.degree < ↑n → p.coeff n = 0 The theorem `Polynomial.coeff_eq_zero_of_degree_lt` states that for any semiring `R`, natural number `n`, and polynomial `p` of type `R`, if the degree of `p` (the highest power of `X` that appears in `p`) is less than `n`, then the coefficient of `X^n` in `p` is zero. In other words, there are no terms in `p` with `X` to the power of `n` or greater. More concisely: For any semiring `R`, natural number `n`, and polynomial `p` over `R` in one variable `X` of degree less than `n`, the coefficient of `X^n` in `p` is equal to zero.
`Polynomial.leadingCoeff_mul_monic` theorem Polynomial.leadingCoeff_mul_monic : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).leadingCoeff = p.leadingCoeff This theorem states that for any semiring `R` and any polynomials `p` and `q` in `R`, if `q` is monic (meaning its leading coefficient is 1), then the leading coefficient of the product `p * q` is the same as the leading coefficient of `p`. In other words, multiplying a polynomial by a monic polynomial does not change the leading coefficient of the original polynomial. More concisely: The leading coefficient of the product of a polynomial and a monic polynomial is equal to the leading coefficient of the original polynomial.
`Polynomial.natDegree_le_iff_degree_le` theorem Polynomial.natDegree_le_iff_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n ↔ p.degree ≤ ↑n The theorem `Polynomial.natDegree_le_iff_degree_le` states that for any type `R` with a semiring structure, any polynomial `p` of type `R`, and any natural number `n`, the natural degree of `p` is less than or equal to `n` if and only if the degree of `p` is less than or equal to `n` coerced to the type `WithBot ℕ`. In other words, this theorem creates a bridge between the comparison of the natural degree and the degree (in the `WithBot ℕ` context) of a polynomial. More concisely: For any semiring `R`, polynomial `p` over `R`, and natural number `n`, the natural degree of `p` is less than or equal to `n` if and only if the degree of `p` is less than or equal to `n` when treated as a natural number with a bottom element.
`Polynomial.degree_le_natDegree` theorem Polynomial.degree_le_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ ↑p.natDegree The theorem `Polynomial.degree_le_natDegree` states that for any semiring `R` and any polynomial `p` from this semiring, the degree of `p` (which could be undefined or `⊥`) is always less than or equal to the natural degree of `p` (which is always defined and is a natural number). Here, the degree of a polynomial is the highest power of `X` that appears in it, and the natural degree is a forced version of the degree, where the degree of the zero polynomial is defined to be zero. More concisely: For any semiring R and polynomial p over R, the degree of p is less than or equal to its natural degree.
`Polynomial.natDegree_mem_support_of_nonzero` theorem Polynomial.natDegree_mem_support_of_nonzero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.natDegree ∈ p.support The theorem `Polynomial.natDegree_mem_support_of_nonzero` states that for any type `R` with a `Semiring` structure and any non-zero polynomial `p` of type `Polynomial R`, the natural degree of `p` (represented as `Polynomial.natDegree p`) is in the support of `p` (denoted as `Polynomial.support p`). Here, the support of a polynomial is the set of all exponents such that the corresponding coefficient of the term with that exponent in the polynomial is non-zero. More concisely: For any non-zero polynomial p of type R in Lean's Polynomial.ynomial structure, the natural degree of p is an element in the support of p.
`Polynomial.degree_X_pow_sub_C` theorem Polynomial.degree_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] {n : ℕ}, 0 < n → ∀ (a : R), (Polynomial.X ^ n - Polynomial.C a).degree = ↑n The theorem `Polynomial.degree_X_pow_sub_C` states that for any ring `R` which is nontrivial, and for any natural number `n` greater than 0 and any element `a` from the ring `R`, the degree of the polynomial obtained by subtracting the constant polynomial `a` from the `n`th power of the polynomial variable `X` is equal to `n`. The degree of the polynomial is the highest power of `X` that appears in the polynomial. More concisely: For any nontrivial ring R and natural number n, the degree of X^n - X^(n-1)a is n, where a is an element of R.*
`Polynomial.ne_zero_of_natDegree_gt` theorem Polynomial.ne_zero_of_natDegree_gt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n < p.natDegree → p ≠ 0 The theorem `Polynomial.ne_zero_of_natDegree_gt` states that for any semiring `R`, and for any polynomial `p` with coefficients in `R`, if there exists a natural number `n` which is less than the natural degree of `p` (`Polynomial.natDegree p`), then `p` cannot be the zero polynomial. In other words, a polynomial with a degree greater than zero is not the zero polynomial. More concisely: A polynomial over a semiring with natural degree greater than zero is not the zero polynomial.
`Polynomial.degree_zero` theorem Polynomial.degree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.degree 0 = ⊥ The theorem `Polynomial.degree_zero` states that for any semiring `R` (a mathematical structure which behaves like the set of natural numbers under addition and multiplication), the degree of the zero polynomial (i.e., the polynomial where all coefficients are zero) is `⊥` (often read as 'bottom'). In other words, the highest power of `X` that appears in the zero polynomial is undefined, since the zero polynomial has no terms. More concisely: The degree of the zero polynomial in a semiring is undefined.
`Polynomial.X_pow_sub_C_ne_zero` theorem Polynomial.X_pow_sub_C_ne_zero : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] {n : ℕ}, 0 < n → ∀ (a : R), Polynomial.X ^ n - Polynomial.C a ≠ 0 The theorem `Polynomial.X_pow_sub_C_ne_zero` states that for any nontrivial ring `R` and positive natural number `n`, the difference between the `n`th power of the polynomial variable `X` and the constant polynomial `a` is not equal to zero. In other words, no matter what constant `a` we choose, subtracting it from `X^n` will never result in a zero polynomial, as long as `n` is a positive integer and `R` is a nontrivial ring. This means that the polynomial `X^n - a` always has some non-zero terms for any choice of `a` and positive `n`. More concisely: For any nontrivial ring R and positive natural number n, the polynomial X^n - a is never equal to the zero polynomial.
`Polynomial.degree_mul'` theorem Polynomial.degree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).degree = p.degree + q.degree The theorem `Polynomial.degree_mul'` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the product of the leading coefficients of `p` and `q` is not zero, then the degree of the product `p * q` is equal to the sum of the degrees of `p` and `q`. In other words, provided the leading coefficients of the polynomials are not both zero, the degree of the multiplication of two polynomials is the sum of their individual degrees. More concisely: For polynomials $p$ and $q$ over a semiring $R$ with non-zero leading coefficients, the degree of their product $p \cdot q$ is equal to the sum of the degrees of $p$ and $q$.
`Polynomial.degree_add_eq_right_of_degree_lt` theorem Polynomial.degree_add_eq_right_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).degree = q.degree The theorem states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the degree of polynomial `p` is less than the degree of polynomial `q`, then the degree of the sum of the polynomials `p` and `q` is equal to the degree of the polynomial `q`. In mathematical terms, this can be written as: if $\deg(p) < \deg(q)$, then $\deg(p + q) = \deg(q)$. More concisely: For any semiring `R`, if `p` and `q` are polynomials over `R` with $\deg(p) < \deg(q)$, then $\deg(p + q) = \deg(q)$.
`Polynomial.Monic.ne_zero` theorem Polynomial.Monic.ne_zero : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : Nontrivial R] {p : Polynomial R}, p.Monic → p ≠ 0 This theorem states that for any semiring `R` that is nontrivial (i.e., `R` has at least two distinct elements), if a polynomial `p` over `R` is monic (meaning its leading coefficient is 1), then `p` must be non-zero. More concisely: In a nontrivial semiring, every monic non-zero polynomial is non-zero.
`Polynomial.degree_quadratic_le` theorem Polynomial.degree_quadratic_le : ∀ {R : Type u} {a b c : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2 This theorem states that for any semiring `R` and any elements `a`, `b`, `c` of `R`, the degree of a polynomial that is constructed as the sum of `a` times the square of the polynomial variable `X`, `b` times `X`, and a constant `c`, is less than or equal to 2. In other words, if we have a quadratic polynomial of the form `aX^2 + bX + c`, its degree won't exceed 2. More concisely: The degree of a quadratic polynomial `aX^2 + bX + c` over a semiring `R` doesn't exceed 2 for any elements `a`, `b`, `c` of `R`.
`Polynomial.leadingCoeff_X_pow_add_C` theorem Polynomial.leadingCoeff_X_pow_add_C : ∀ {R : Type u} [inst : Semiring R] {n : ℕ}, 0 < n → ∀ {r : R}, (Polynomial.X ^ n + Polynomial.C r).leadingCoeff = 1 This theorem states that for any semiring `R`, any natural number `n` greater than 0, and any element `r` of `R`, the leading coefficient of the polynomial formed by adding `r` times the constant polynomial to the `n`-th power of the polynomial variable `X`, is equal to 1. In more mathematical terms, for any polynomial of the form `X^n + r`, where `n` is a positive natural number and `r` is a constant, the coefficient of the highest degree term (`X^n`) is 1. More concisely: For any semiring `R` and natural number `n` greater than 0, the leading coefficient of the polynomial `X^n + r` (where `r` is an element of `R`) is equal to 1.
`Polynomial.natDegree_X_sub_C` theorem Polynomial.natDegree_X_sub_C : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] (x : R), (Polynomial.X - Polynomial.C x).natDegree = 1 := by sorry The theorem `Polynomial.natDegree_X_sub_C` states that for any type `R` that forms a ring and is nontrivial, and for any element `x` of `R`, the natural degree of the polynomial obtained by subtracting the constant polynomial `x` from the polynomial variable `X` is always 1. In other words, the degree of the polynomial `X - x` is 1 for any `x` in a nontrivial ring `R`. More concisely: For any nontrivial ring R and its element x, the degree of the polynomial X - x is 1.
`Polynomial.natDegree_le_of_degree_le` theorem Polynomial.natDegree_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.degree ≤ ↑n → p.natDegree ≤ n The theorem `Polynomial.natDegree_le_of_degree_le` states that for any semiring `R`, polynomial `p` of type `R`, and natural number `n`, if the degree of `p` (the highest power of `X` appearing in `p`) is less than or equal to `n`, then the natural degree of `p` (which is the forced degree of `p` to natural numbers, with the degree of a zero polynomial defined as 0) is also less than or equal to `n`. Essentially, this theorem provides the condition under which the natural degree of a polynomial is less than or equal to a given natural number, based on its degree. More concisely: For any semiring `R`, polynomial `p` of degree `d` over `R`, and natural number `n`, if `d` ≤ `n`, then the natural degree of `p` is also less than or equal to `n`.
`Polynomial.natDegree_C_mul_X` theorem Polynomial.natDegree_C_mul_X : ∀ {R : Type u} [inst : Semiring R] (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X).natDegree = 1 The theorem `Polynomial.natDegree_C_mul_X` states that for any non-zero element `a` of a semiring `R`, the natural degree of the polynomial obtained by multiplying the constant polynomial `a` and the polynomial variable `X` is equal to 1. This essentially means that the degree of a monomial (a product of a constant and a variable) is the power to which the variable is raised, which in this case is 1. More concisely: The natural degree of the polynomial resulting from multiplying a non-zero constant `a` with the polynomial variable `X` is 1.
`Polynomial.coeff_eq_zero_of_natDegree_lt` theorem Polynomial.coeff_eq_zero_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree < n → p.coeff n = 0 The theorem `Polynomial.coeff_eq_zero_of_natDegree_lt` states that for any type `R` equipped with a semiring structure, any polynomial `p` over `R`, and any natural number `n`, if `n` is greater than the natural degree of `p` (`Polynomial.natDegree p < n`), then the coefficient of `X^n` in `p` (`Polynomial.coeff p n`) is equal to zero. In other words, if the degree of a polynomial is less than a given natural number, the polynomial's coefficient for the term with that exponent is zero. More concisely: For any polynomial `p` over a semiring `R` and natural number `n` greater than its degree `Polynomial.natDegree p`, the coefficient `Polynomial.coeff p n` is equal to zero.
`Polynomial.natDegree_mul'` theorem Polynomial.natDegree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).natDegree = p.natDegree + q.natDegree The theorem `Polynomial.natDegree_mul'` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the product of the leading coefficients of `p` and `q` is nonzero, then the natural degree of the product of `p` and `q` is equal to the sum of the natural degrees of `p` and `q`. Here, the "leading coefficient" of a polynomial is the coefficient of the highest power of `X` in the polynomial, and the "natural degree" of a polynomial forces the degree of the polynomial to ℕ by defining the natural degree of 0 as 0. More concisely: If `R` is a semiring and `p(X)` and `q(X)` are polynomials over `R` with nonzero product of leading coefficients, then the natural degree of `p(X) * q(X)` equals the sum of the natural degrees of `p(X)` and `q(X)`.
`Polynomial.degree_lt_wf` theorem Polynomial.degree_lt_wf : ∀ {R : Type u} [inst : Semiring R], WellFounded fun p q => p.degree < q.degree := by sorry The theorem `Polynomial.degree_lt_wf` states that for all semirings `R`, the relation "having a strictly lesser degree" (`Polynomial.degree p < Polynomial.degree q`) on the set of polynomials with coefficients in `R` is well-founded. In other words, it implies that there are no infinite decreasing sequences of polynomial degrees. This is a fundamental property in the theory of polynomials which is used in many arguments involving induction on the degree of a polynomial. More concisely: The relation "having a strictly lesser degree" on polynomials over a semiring is a well-founded relation.
`Polynomial.natDegree_sub_C` theorem Polynomial.natDegree_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {a : R}, (p - Polynomial.C a).natDegree = p.natDegree The theorem `Polynomial.natDegree_sub_C` states that for any given ring `R`, any polynomial `p` over `R`, and any element `a` of `R`, the natural degree of the polynomial resulting from subtracting the constant polynomial `a` from `p` is equal to the natural degree of the original polynomial `p`. In other words, subtracting a constant from a polynomial does not change its natural degree. More concisely: The natural degree of a polynomial's difference with a constant polynomial is equal to the natural degree of the original polynomial.
`Polynomial.degree_eq_bot` theorem Polynomial.degree_eq_bot : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree = ⊥ ↔ p = 0 := by sorry This theorem states that for any type `R` which is a semiring and any polynomial `p` over `R`, the degree of the polynomial `p` is equal to `⊥` (which represents an undefined or lowest possible degree) if and only if the polynomial `p` is zero. In mathematical terms, the degree of a polynomial is undefined or at its lowest possible value precisely when the polynomial itself is zero. More concisely: For any semiring `R` and polynomial `p` over `R`, the degree of `p` is 0 if and only if `p` is the zero polynomial.
`Polynomial.degree_mul_le` theorem Polynomial.degree_mul_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).degree ≤ p.degree + q.degree The theorem `Polynomial.degree_mul_le` states that for any type `R` that is a semiring, and for any two polynomials `p` and `q` over that semiring, the degree of the product of `p` and `q` is less than or equal to the sum of the degrees of `p` and `q`. In other words, the highest power of `X` that appears in the polynomial resulting from the multiplication of `p` and `q` cannot exceed the sum of the highest powers of `X` that appear in `p` and `q` respectively. More concisely: For any semiring R and polynomials p and q over R, the degree of the product p q is less than or equal to the sum of the degrees of p and q.
`Polynomial.nonempty_support_iff` theorem Polynomial.nonempty_support_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.Nonempty ↔ p ≠ 0 This theorem states that for any semiring `R` and any polynomial `p` over `R`, the support set of `p` (i.e., the set of all `n` such that the `n`-th power of `X` has a non-zero coefficient in `p`) is nonempty if and only if the polynomial `p` is not the zero polynomial. In other words, a polynomial has a non-empty support iff it isn't the zero polynomial. More concisely: A polynomial over a semiring is non-zero if and only if its support set is non-empty.
`Polynomial.natDegree_monomial` theorem Polynomial.natDegree_monomial : ∀ {R : Type u} [inst : Semiring R] [inst_1 : DecidableEq R] (i : ℕ) (r : R), ((Polynomial.monomial i) r).natDegree = if r = 0 then 0 else i This theorem states that for any type `R` that is a semiring and has decidable equality, and for any natural number `i` and any element `r` of `R`, the natural degree of the polynomial obtained by applying the monomial `i` to `r` is `i` if `r` is not zero; otherwise, if `r` is zero, the natural degree is zero. Essentially, this theorem asserts that the degree of a monomial `a * X^i` is `i`, unless the coefficient `a` is zero, in which case the degree is also zero. More concisely: For any semiring `R` with decidable equality and any `i` in `ℕ` and `r` in `R`, the natural degree of the polynomial `i r` is `i` if `r` is nonzero, and is zero otherwise.*
`Polynomial.degree_neg` theorem Polynomial.degree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).degree = p.degree This theorem states that for every polynomial `p` defined over a ring `R`, the degree of the negation of `p` (denoted as `-p`) is the same as the degree of `p` itself. In mathematical terms, if `p` is a polynomial over a ring `R`, then the largest exponent of `x` that appears in `-p` is the same as the largest exponent of `x` that appears in `p`. This is true regardless of whether `p` is a non-zero polynomial or the zero polynomial. More concisely: The degree of the negation of a polynomial over a ring is equal to the degree of the polynomial itself.
`Polynomial.degree_X_pow_le` theorem Polynomial.degree_X_pow_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).degree ≤ ↑n := by sorry The theorem `Polynomial.degree_X_pow_le` states that, for any semiring `R` and natural number `n`, the degree of the polynomial which is the variable `X` raised to the power `n` (`Polynomial.X ^ n`) is less than or equal to `n`. In other words, the highest power of `X` that appears in the polynomial `X^n` is no greater than `n`. More concisely: For any semiring R and natural number n, the degree of the polynomial X^n is less than or equal to n.
`Polynomial.degree_lt_iff_coeff_zero` theorem Polynomial.degree_lt_iff_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (n : ℕ), f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0 This theorem states that for any semiring `R` and any polynomial `f` over `R`, the degree of `f` is less than a given natural number `n` if and only if all the coefficients of `f` for powers of `X` greater than or equal to `n` are zero. In other words, the highest power of `X` that has a non-zero coefficient in `f` is less than `n`. More concisely: For any semiring `R` and polynomial `f` over `R` in the indeterminate `X`, the degree of `f` is less than `n` if and only if all coefficients of `X^i` with `i ≥ n` in `f` are zero.
`Polynomial.natDegree_eq_of_degree_eq` theorem Polynomial.natDegree_eq_of_degree_eq : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {q : Polynomial S}, p.degree = q.degree → p.natDegree = q.natDegree The theorem states that for any two polynomials `p` and `q` over two potentially different semirings `R` and `S`, if the degree of `p` (the highest power of `X` that appears in `p`) is equal to the degree of `q` (the highest power of `X` that appears in `q`), then the natural degree of `p` (the degree forced to natural numbers, where the degree of the zero polynomial is defined as 0) is equal to the natural degree of `q`. More concisely: If two polynomials `p` and `q` over semirings `R` and `S` have equal degrees, then their natural degrees are equal.
`Polynomial.degree_eq_iff_natDegree_eq` theorem Polynomial.degree_eq_iff_natDegree_eq : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p ≠ 0 → (p.degree = ↑n ↔ p.natDegree = n) The theorem `Polynomial.degree_eq_iff_natDegree_eq` states that for any semiring `R` and any non-zero polynomial `p` from `R`, the degree of `p` is equal to `n` (in the option type with bottom, represented as `↑n`) if and only if the natural degree of `p` is `n`. Here, the degree of a polynomial is the highest exponent that appears in it, and the natural degree is the same except that it is defined to be 0 for the zero polynomial. More concisely: For any semiring R and non-zero polynomial p from R, the degree and natural degree are equal if and only if p has a highest exponent of degree n.
`Polynomial.natDegree_le_natDegree` theorem Polynomial.natDegree_le_natDegree : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p : Polynomial R} [inst_1 : Semiring S] {q : Polynomial S}, p.degree ≤ q.degree → p.natDegree ≤ q.natDegree This theorem, `Polynomial.natDegree_le_natDegree`, asserts that for any two polynomials `p` and `q`, over semirings `R` and `S` respectively, if the degree of `p` is less than or equal to the degree of `q`, then the natural degree of `p` is also less than or equal to the natural degree of `q`. In other words, the inequality between the degrees of two polynomials is preserved when those degrees are converted to natural numbers. This result holds irrespective of the types of semirings, `R` and `S`, over which the polynomials are defined. More concisely: For any polynomials `p` and `q` over semirings `R` and `S`, respectively, if the degree of `p` is less than or equal to the degree of `q`, then the natural degrees of `p` and `q` are equal or the natural degree of `p` is less than the natural degree of `q`.
`Polynomial.X_sub_C_ne_zero` theorem Polynomial.X_sub_C_ne_zero : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] (r : R), Polynomial.X - Polynomial.C r ≠ 0 The theorem `Polynomial.X_sub_C_ne_zero` states that for any type `R` that forms a ring and is nontrivial (i.e., it has at least two distinct elements), and for any element `r` of `R`, the polynomial `X - C r` (where `X` is the polynomial variable and `C r` is the constant polynomial `r`) is not equal to zero. This means that subtracting a constant polynomial from the polynomial variable always yields a non-zero polynomial. More concisely: For any nontrivial ring `R` and its element `r`, the polynomial `X - C r` is never equal to the zero polynomial.
`Polynomial.degree_add_eq_left_of_degree_lt` theorem Polynomial.degree_add_eq_left_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.degree < p.degree → (p + q).degree = p.degree The theorem `Polynomial.degree_add_eq_left_of_degree_lt` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the degree of polynomial `q` is strictly less than the degree of polynomial `p`, then the degree of the sum of polynomial `p` and polynomial `q` equals the degree of polynomial `p`. In other words, when adding two polynomials, if one has a lower degree than the other, the degree of the resulting polynomial will be the same as the degree of the higher-degree polynomial. More concisely: For any semiring R and polynomials p and q over R with deg(q) < deg(p), the degree of p + q equals deg(p).
`Polynomial.leadingCoeff_C_mul_X_pow` theorem Polynomial.leadingCoeff_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ), (Polynomial.C a * Polynomial.X ^ n).leadingCoeff = a This theorem states that for any semiring `R`, and for any element `a` from `R` and any natural number `n`, the leading coefficient of the polynomial obtained by multiplying the constant polynomial `a` with `X` raised to the power `n` is `a`. In other words, if you have a polynomial that is simply a constant times a power of `X`, the leading coefficient (the coefficient of the highest power of `X`) is just that constant. More concisely: For any semiring `R` and element `a` from `R`, the leading coefficient of the polynomial `a X^n` is `a`.*
`Polynomial.degree_X_pow_add_C` theorem Polynomial.degree_X_pow_add_C : ∀ {R : Type u} [inst : Nontrivial R] [inst : Semiring R] {n : ℕ}, 0 < n → ∀ (a : R), (Polynomial.X ^ n + Polynomial.C a).degree = ↑n The theorem `Polynomial.degree_X_pow_add_C` states that for any non-trivial semiring `R` and any positive integer `n`, the degree of the polynomial that results from adding a constant `a` (from `R`) to the `n`th power of the polynomial variable `X` is `n`. In other words, if we have a polynomial formed by adding a constant to `X` raised to a positive power, the degree of that polynomial will be equal to the power to which `X` was raised, irrespective of the constant added. This is expressed mathematically as $\text{degree}(X^n + a) = n$ for $n > 0$ and $a \in R$. More concisely: The degree of a polynomial of the form `X^n + a`, where `X` is a polynomial variable, `n` is a positive integer, and `a` is a constant from a non-trivial semiring, is equal to `n`.
`Polynomial.ne_zero_of_degree_gt` theorem Polynomial.ne_zero_of_degree_gt : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : WithBot ℕ}, n < p.degree → p ≠ 0 This theorem states that for any type `R` with a semiring structure and any polynomial `p` of type `R`, if there is a value `n` of type "WithBot ℕ" which is less than the degree of the polynomial `p`, then the polynomial `p` cannot be zero. In simpler terms, if a polynomial has a degree greater than a certain number `n`, then that polynomial cannot be the zero polynomial. Here, "WithBot ℕ" is a type that adds a 'bottom' element, typically denoted as `⊥`, to the natural numbers, and the degree of the zero polynomial is defined as this `⊥` value. More concisely: For any semiring `R` and polynomial `p` of degree greater than the smallest natural number `n` in `R`, `p` is not the zero polynomial.
`Polynomial.degree_add_le` theorem Polynomial.degree_add_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).degree ≤ max p.degree q.degree The theorem `Polynomial.degree_add_le` states that for any given semiring `R` and any two polynomials `p` and `q` over `R`, the degree of the sum of the polynomials `(p + q)` is less than or equal to the maximum of the degrees of `p` and `q`. In other words, adding two polynomials does not increase the degree beyond the highest degree of the original polynomials. More concisely: For any semiring R and polynomials p and q over R, the degree of p + q is less than or equal to the maximum of the degrees of p and q.
`Polynomial.degree_X_sub_C` theorem Polynomial.degree_X_sub_C : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] (a : R), (Polynomial.X - Polynomial.C a).degree = 1 := by sorry The theorem `Polynomial.degree_X_sub_C` states that for any ring `R` that is nontrivial, and for any element `a` in `R`, the degree of the polynomial `(Polynomial.X - Polynomial.C a)` is 1. Here, `Polynomial.X` represents the polynomial variable and `Polynomial.C a` is the constant polynomial `a`. This means that the highest power of the polynomial variable that appears in the polynomial resulting from subtracting the constant polynomial `a` from the polynomial variable is 1. More concisely: For any nontrivial ring R and element a in R, the degree of the polynomial (X - C a) is 1.
`Polynomial.le_natDegree_of_ne_zero` theorem Polynomial.le_natDegree_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → n ≤ p.natDegree The theorem `Polynomial.le_natDegree_of_ne_zero` states that for any semiring `R`, natural number `n`, and polynomial `p` with coefficients in `R`, if the coefficient of `X^n` in `p` is not zero, then `n` is less than or equal to the natural degree of `p`. The natural degree of a polynomial is a forced version of the degree of the polynomial into natural numbers, where the degree of the zero polynomial is defined to be zero. More concisely: If a polynomial `p` of degree `n` over a semiring `R` has a non-zero coefficient for `X^k` with `k = n`, then `k` is the natural degree of `p`.
`Polynomial.coeff_natDegree_eq_zero_of_degree_lt` theorem Polynomial.coeff_natDegree_eq_zero_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → p.coeff q.natDegree = 0 This theorem states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the degree of `p` is less than the degree of `q`, then the coefficient of the term in `p` with exponent equal to the "natural degree" of `q` (i.e., the degree of `q` coerced to a natural number) is zero. This means that `p` does not have a term with the same degree as the highest degree term of `q`. More concisely: For any semiring `R` and polynomials `p` and `q` over `R` with `deg p < deg q`, the coefficient of the term of highest degree in `p` is zero.
`Polynomial.degree_monomial_le` theorem Polynomial.degree_monomial_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).degree ≤ ↑n This theorem states that for any semiring `R`, any natural number `n`, and any element `a` of `R`, the degree of the monomial `a * X^n` is less than or equal to `n`. In other words, the highest power of `X` that appears in the polynomial `a * X^n` is at most `n`. This is a characteristic property of monomials in any polynomial algebra over a semiring. More concisely: For any semiring `R`, the degree of the monomial `a X^n` with `a` in `R` and `n` a natural number, is bounded by `n`.*
`Polynomial.natDegree_eq_of_degree_eq_some` theorem Polynomial.natDegree_eq_of_degree_eq_some : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.degree = ↑n → p.natDegree = n This theorem states that for any polynomial `p` over a semiring `R`, if the degree of `p` (which could be `⊥` for the zero polynomial) is equal to `n` (where `n` is a natural number represented in the lifting of natural numbers to include `⊥`), then the natural degree of `p` (which forces the degree of `p` to natural numbers by setting the degree of the zero polynomial to `0`) is also `n`. In other words, if the degree of the polynomial, which could be potentially undefined (in the case of the zero polynomial), is defined and equal to `n`, then the natural degree, which is always defined, is also `n`. More concisely: For any polynomial `p` over a semiring `R` with degree `n`, the natural degree of `p` equals `n`.
`Polynomial.natDegree_add_le` theorem Polynomial.natDegree_add_le : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p + q).natDegree ≤ max p.natDegree q.natDegree The theorem `Polynomial.natDegree_add_le` states that for any semiring `R` and for any two polynomials `p` and `q` over `R`, the natural degree of the sum of `p` and `q` is less than or equal to the maximum of the natural degrees of `p` and `q`. In other words, when you add two polynomials, the degree of the resulting polynomial won't exceed the higher of the two original polynomial's degrees. More concisely: For any semiring R and polynomials p and q over R, the natural degree of p + q is less than or equal to max (deg p, deg q).
`Polynomial.natDegree_add_C` theorem Polynomial.natDegree_add_C : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R}, (p + Polynomial.C a).natDegree = p.natDegree := by sorry This theorem states that for any semiring `R`, any polynomial `p` over `R`, and any element `a` from `R`, the natural degree of the sum of the polynomial `p` and the constant polynomial `a` is equal to the natural degree of the polynomial `p`. In other words, adding a constant to a polynomial does not change its natural degree. More concisely: The natural degree of a polynomial `p` over a semiring `R` plus a constant polynomial `a` over `R` equals the natural degree of `p`.
`Polynomial.degree_le_of_natDegree_le` theorem Polynomial.degree_le_of_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.natDegree ≤ n → p.degree ≤ ↑n This theorem, `Polynomial.degree_le_of_natDegree_le`, states that for any type `R` that is a semiring and any polynomial `p` of type `R` and natural number `n`, if the natural degree of the polynomial `p` is less than or equal to `n`, then the degree of polynomial `p` is also less than or equal to `n`. In other words, it states that the degree of a polynomial, which is the highest power of `X` that appears in the polynomial, is less than or equal to a certain natural number if the natural degree of the polynomial, which is the same as the degree but defined to be zero for the zero polynomial, is less than or equal to that number. More concisely: For any semiring `R` and polynomial `p` of degree `n` over `R` with natural degree `m`, if `m` is less than or equal to `n`, then the degree of `p` is also less than or equal to `n`.
`Polynomial.degree_monomial` theorem Polynomial.degree_monomial : ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → ((Polynomial.monomial n) a).degree = ↑n This theorem states that for any semiring `R` and any element `a` of `R` which is not zero, and any natural number `n`, the degree of the polynomial produced by multiplying `a` by `X^n` (where `X` is an indeterminate) is `n`. In other words, the degree of a monomial `a * X^n` is `n`, provided `a` is not zero. More concisely: For any semiring `R`, and any non-zero element `a` in `R` and natural number `n`, the degree of the polynomial `a X^n` is `n`.*
`Polynomial.degree_X_le` theorem Polynomial.degree_X_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.degree ≤ 1 The theorem `Polynomial.degree_X_le` states that for any semiring `R`, the degree of the polynomial `Polynomial.X` is less than or equal to 1. In essence, this theorem asserts that the degree of the polynomial variable, denoted as `X`, is always 1 or less in any given semiring. Here, `Polynomial.X` represents a polynomial with a single term of degree 1, which is why its degree cannot be more than 1. More concisely: For any semiring R, the degree of the polynomial variable X in the context of the Polynomial type is at most 1.
`Polynomial.leadingCoeff_mul` theorem Polynomial.leadingCoeff_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] (p q : Polynomial R), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff The theorem `Polynomial.leadingCoeff_mul` states that for any given semiring `R` with no zero divisors, and any two polynomials `p` and `q` over `R`, the leading coefficient (the coefficient of the highest power of `X`) of the product of `p` and `q` is equal to the product of the leading coefficients of `p` and `q`. In other words, if we multiply two polynomials, the leading coefficient of the resulting polynomial is the multiplication of the leading coefficients of the original polynomials. This can be expressed mathematically as `leadCoeff(p * q) = leadCoeff(p) * leadCoeff(q)`. More concisely: For polynomials $p$ and $q$ over a semiring $R$ without zero divisors, the leading coefficient of their product $pq$ is equal to the product of their leading coefficients. In Lean notation: `leadCoeff (p * q) = leadCoeff p * leadCoeff q`.
`Polynomial.degree_sum_le` theorem Polynomial.degree_sum_le : ∀ {R : Type u} [inst : Semiring R] {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial R), (s.sum fun i => f i).degree ≤ s.sup fun b => (f b).degree The theorem `Polynomial.degree_sum_le` states that for any semiring `R`, any finite set `s` of type `ι`, and any function `f` that maps elements of `ι` to polynomials in `R`, the degree of the sum of polynomials (which is obtained by summing the polynomials that result from applying `f` to each element in `s`) is less than or equal to the supremum of the degrees of the polynomials for each element in `s`. In other words, the degree of the sum of these polynomials is not larger than the highest degree of these polynomials. More concisely: For any semiring R, finite set ι, and function f from ι to polynomials over R, the degree of the sum of the polynomials in the image of f is less than or equal to the supremum of the degrees of the polynomials in the image of f.
`Polynomial.monic_one` theorem Polynomial.monic_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.Monic 1 The theorem `Polynomial.monic_one` states that for any type `R` that has a semiring structure, the polynomial `1` is `Monic`. In other words, the polynomial with constant term `1` is considered `Monic` in any semiring, since its leading coefficient is indeed `1`. More concisely: In any semiring, the constant polynomial 1 is monic.
`Polynomial.degree_lt_degree` theorem Polynomial.degree_lt_degree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.natDegree < q.natDegree → p.degree < q.degree This theorem states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the natural degree of `p` is less than the natural degree of `q`, then the degree of `p` is also less than the degree of `q`. The natural degree of a polynomial is defined as the highest power of `X` that appears in the polynomial, or `0` in the case of the zero polynomial. The degree of a polynomial is similarly the highest power of `X` that appears, but is undefined for the zero polynomial. More concisely: If `R` is a semiring and `p` and `q` are polynomials over `R` with `deg p < deg q`, then the natural degree of `p` is strictly less than the natural degree of `q`.
`Polynomial.degree_cubic_le` theorem Polynomial.degree_cubic_le : ∀ {R : Type u} {a b c d : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree ≤ 3 This theorem states that for any type `R` that forms a semiring and any four elements `a`, `b`, `c`, and `d` of `R`, the degree of the polynomial `aX^3 + bX^2 + cX + d` (where `a`, `b`, `c`, and `d` are coefficients and `X` is the polynomial variable) is less than or equal to 3. In other words, in a cubic polynomial, the highest power of `X` that appears in the polynomial is 3. More concisely: The degree of a cubic polynomial `aX^3 + bX^2 + cX + d` over a semiring `R` is bounded by 3, where `a`, `b`, `c`, `d` are elements of `R` and `X` is the polynomial variable.
`Polynomial.Monic.degree_mul` theorem Polynomial.Monic.degree_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).degree = p.degree + q.degree The theorem `Polynomial.Monic.degree_mul` states that for any semiring `R` and any two polynomials `p` and `q` from that semiring, if `q` is a monic polynomial (meaning its leading coefficient is `1`), then the degree of the product of `p` and `q` is the sum of the degrees of `p` and `q`. The degree of a polynomial is the largest exponent of `X` that appears in the polynomial. More concisely: For any semiring R and monic polynomials p and q from R, the degree of their product is the sum of the degrees of p and q.
`Polynomial.natDegree_zero` theorem Polynomial.natDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.natDegree 0 = 0 This theorem states that, for any type `R` that is a semiring, the natural degree of the zero polynomial is zero. In other words, when the polynomial is `0`, its degree is also `0`. This adheres to the general mathematical principle that the degree of the zero polynomial is defined to be zero. More concisely: For any semiring type R, the degree of the zero polynomial is 0.
`Polynomial.coeff_natDegree` theorem Polynomial.coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeff p.natDegree = p.leadingCoeff The theorem `Polynomial.coeff_natDegree` states that for all polymonials `p` over a semiring `R`, the coefficient of the term with degree equal to the natural degree of `p` is the same as the leading coefficient of `p`. In other words, in any polynomial, the coefficient of the term with the highest power of `X` (the leading term) is the same whether we retrieve it using the `coeff` function with the natural degree of the polynomial as the argument, or directly using the `leadingCoeff` function. More concisely: The theorem `Polynomial.coeff_natDegree` asserts that the coefficient of the term of highest degree in a polynomial equals the leading coefficient, i.e., `coeff p (natDegree p) = leadingCoeff p`.
`Polynomial.leadingCoeff_eq_zero` theorem Polynomial.leadingCoeff_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff = 0 ↔ p = 0 The theorem `Polynomial.leadingCoeff_eq_zero` states that for all `R` of type `u` with a semiring structure, and for any polynomial `p` over `R`, the leading coefficient of `p` is zero if and only if `p` is the zero polynomial. The leading coefficient of a polynomial is defined as the coefficient of the highest power of `X` in the polynomial. Therefore, this theorem is essentially stating that a polynomial is zero if and only if its highest power term's coefficient is zero. More concisely: A polynomial over a semiring is the zero polynomial if and only if its leading coefficient is zero.
`Polynomial.le_degree_of_ne_zero` theorem Polynomial.le_degree_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → ↑n ≤ p.degree This theorem states that for any semiring `R`, any natural number `n`, and any polynomial `p` over `R`, if the coefficient of `X^n` in `p` (denoted `Polynomial.coeff p n`) is not zero, then `n` is less than or equal to the degree of the polynomial `p` (denoted `Polynomial.degree p`). In other words, if a term with `X^n` is present (and has non-zero coefficient) in the polynomial, the degree of the polynomial is at least `n`. More concisely: For any semiring `R`, if `p` is a polynomial over `R` with non-zero coefficient for `X^n` where `n` is less than or equal to the degree of `p`, then `n` is equal to the degree of `p`. (Note: The statement in the description seems to have a mistake as it only guarantees that the degree of `p` is at least `n`, not equal to `n`.)
`Polynomial.degree_sub_le` theorem Polynomial.degree_sub_le : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), (p - q).degree ≤ max p.degree q.degree The theorem `Polynomial.degree_sub_le` states that for any two polynomials `p` and `q` over a ring `R`, the degree of the polynomial resulting from subtracting `q` from `p` (denoted `p - q`) is less than or equal to the maximum of the degrees of `p` and `q`. In other words, the highest power of `X` that appears in the polynomial `p - q` is no greater than the highest power of `X` that appears in either `p` or `q`. More concisely: The degree of the polynomial `p - q` is less than or equal to the maximum degree of `p` and `q`.
`Polynomial.degree_le_zero_iff` theorem Polynomial.degree_le_zero_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 0 ↔ p = Polynomial.C (p.coeff 0) The theorem `Polynomial.degree_le_zero_iff` establishes an equivalence condition for a polynomial in a given semiring. It states that for any polynomial `p` over a semiring `R`, the degree of the polynomial `p` is less than or equal to zero if and only if `p` is equal to the constant polynomial whose coefficient is the coefficient of `p` at degree 0. In other words, a polynomial has degree at most zero if and only if it is a constant polynomial, where the constant term is the coefficient of the zeroth degree term of the polynomial. More concisely: A polynomial over a semiring has degree at most zero if and only if it is equal to the constant polynomial with coefficient equal to its zeroth degree term.
`Polynomial.degree_C_mul_X_pow_le` theorem Polynomial.degree_C_mul_X_pow_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n The theorem `Polynomial.degree_C_mul_X_pow_le` states that for any semiring `R`, any natural number `n`, and any element `a` of `R`, the degree of the polynomial obtained by multiplying the constant polynomial `a` with the `n`th power of the polynomial variable `X` is at most `n`. In other words, if we form a polynomial by multiplying a constant by `X` raised to some power, the degree of that polynomial (the highest exponent that appears) cannot exceed that power. More concisely: For any semiring R, natural number n, and element a in R, the degree of the polynomial a X^n is at most n.*
`Polynomial.sum_over_range` theorem Polynomial.sum_over_range : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S}, (∀ (n : ℕ), f n 0 = 0) → p.sum f = (Finset.range (p.natDegree + 1)).sum fun a => f a (p.coeff a) This theorem states that for any semiring `R`, additively commutative monoid `S`, and a polynomial `p` over `R`, given a function `f` mapping from natural numbers and elements of `R` to `S` that maps any natural number and zero to zero, the sum of `f(n, p.coeff n)` over the support of `p` can be reexpressed as the sum of `f(a, p.coeff a)` over the range from `0` to `p.natDegree + 1`. In other words, the sum over the non-zero coefficients of the polynomial can be computed as a sum over a range that extends one past the degree of the polynomial. More concisely: For any semiring `R`, additively commutative monoid `S`, polynomial `p` over `R`, and function `f` from natural numbers and `R` to `S` with `f(n, 0) = 0`, the sum of `f(n, p.coeff n)` over the support of `p` equals the sum of `f(a, p.coeff a)` for `0 ≤ a ≤ p.natDegree + 1`.
`Polynomial.degree_C_mul_X_pow` theorem Polynomial.degree_C_mul_X_pow : ∀ {R : Type u} {a : R} [inst : Semiring R] (n : ℕ), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).degree = ↑n := by sorry The theorem `Polynomial.degree_C_mul_X_pow` states that for any semiring `R`, any element `a` of `R` and any natural number `n`, if `a` is not zero, then the degree of the polynomial obtained by multiplying the constant polynomial `a` with the `n`th power of the polynomial variable `X` is `n`. In other words, if we have a non-zero constant times a power of the polynomial variable, the degree of the resulting polynomial is just the exponent of the power. More concisely: For any semiring R and natural number n, the degree of the polynomial a X^n is n, where a is a non-zero element of R.*
`Polynomial.natDegree_one` theorem Polynomial.natDegree_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.natDegree 1 = 0 This theorem states that for any type `R` that is a semiring, the natural degree of the polynomial `1` is `0`. In mathematical terms, this means that the degree of the constant polynomial `1` (which is a polynomial that does not depend on the variable) in any semiring is `0`. This is consistent with the general rule that the degree of a nonzero constant polynomial is `0`. More concisely: For any semiring R, the constant polynomial 1 has degree 0.
`Polynomial.leadingCoeff_neg` theorem Polynomial.leadingCoeff_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).leadingCoeff = -p.leadingCoeff The theorem `Polynomial.leadingCoeff_neg` states that for any given polynomial `p` over a ring `R`, the leading coefficient of the negation of `p` (denoted as `-p`) equals the negation of the leading coefficient of `p`. Here, the leading coefficient of a polynomial is the coefficient of the highest power of `X` in the polynomial. More concisely: The leading coefficient of the negation of a polynomial is the negative of the leading coefficient of the original polynomial.
`Polynomial.degree_X_pow` theorem Polynomial.degree_X_pow : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ), (Polynomial.X ^ n).degree = ↑n The theorem `Polynomial.degree_X_pow` states that for any semiring `R` (a type of algebraic structure) that is not trivial (i.e., containing at least two distinct elements), and for any natural number `n`, the degree of the polynomial obtained by raising the polynomial variable `X` to the power of `n` is equal to `n`. In mathematical terms, this is saying that the degree of the polynomial `X^n` is `n`. More concisely: For any semiring R with at least two elements and natural number n, the degree of the polynomial X^n is n.
`Polynomial.natDegree_C` theorem Polynomial.natDegree_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).natDegree = 0 This theorem states that for any semiring `R` and any element `a` of `R`, the natural degree of the constant polynomial `C a` is 0. In other words, the degree of a constant polynomial, when considered as a natural number, is always zero, regardless of the semiring in which the polynomial is defined or the specific constant value of the polynomial. More concisely: The natural degree of a constant polynomial is always 0 in any semiring.
`Polynomial.degree_eq_natDegree` theorem Polynomial.degree_eq_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.degree = ↑p.natDegree This theorem states that for any given non-zero polynomial `p` over a semiring `R`, the degree of `p` is equal to the natural number degree of `p`. In mathematical terms, if 'p' is not equal to zero, then the degree of 'p', which is the highest power of 'X' that appears in 'p' (possibly with a bottom element for the zero polynomial), is equal to the natural number degree of 'p', which forces the degree into the set of natural numbers, defining the degree of the zero polynomial as 0. More concisely: For any non-zero polynomial `p` over a semiring `R`, the degree of `p` equals the natural number degree of `p`.
`Polynomial.degree_C` theorem Polynomial.degree_C : ∀ {R : Type u} {a : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a).degree = 0 := by sorry The theorem `Polynomial.degree_C` states that for any type `R` and element `a` of that type, as long as `R` is a semiring and `a` is not zero, the degree of the constant polynomial `C a` is 0. In other words, when we have a polynomial that is simply a constant (non-zero) value, the highest power of `X` that appears in the polynomial is 0, as there are no `X` terms in the polynomial. More concisely: For any semiring `R` and non-zero element `a` in `R`, the degree of the constant polynomial `C a` is 0.
`Polynomial.coeff_mul_degree_add_degree` theorem Polynomial.coeff_mul_degree_add_degree : ∀ {R : Type u} [inst : Semiring R] (p q : Polynomial R), (p * q).coeff (p.natDegree + q.natDegree) = p.leadingCoeff * q.leadingCoeff The theorem `Polynomial.coeff_mul_degree_add_degree` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, the coefficient of the term in the product `p * q` with degree equal to the sum of the degrees of `p` and `q` is equal to the product of the leading coefficients of `p` and `q`. The leading coefficient of a polynomial is the coefficient of its highest-degree term. More concisely: Given polynomials $p$ and $q$ over a semiring $R$, the coefficient of the term of degree $\degree p + \degree q$ in the product $pq$ is equal to the product of their leading coefficients.
`Polynomial.eq_X_add_C_of_degree_le_one` theorem Polynomial.eq_X_add_C_of_degree_le_one : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 1 → p = Polynomial.C (p.coeff 1) * Polynomial.X + Polynomial.C (p.coeff 0) The theorem `Polynomial.eq_X_add_C_of_degree_le_one` states that for any polynomial `p` over a semiring `R` where the degree of `p` is less than or equal to 1, `p` can be expressed as the sum of a monomial of degree 1 and a constant. More specifically, `p` is equal to the product of the constant polynomial of the coefficient of `X` in `p` and the polynomial variable `X`, added to the constant polynomial of the constant term in `p`. In mathematical terms, if the degree of a polynomial `p(X)` is less than or equal to 1, then `p(X) = aX + b`, where `a` is the coefficient of `X` in `p` and `b` is the constant term in `p`. More concisely: For any polynomial `p` of degree less than or equal to 1 over a semiring, `p(X)` equals the product of the coefficient of `X` in `p` and `X`, plus the constant term in `p`.
`Polynomial.degree_sub_lt` theorem Polynomial.degree_sub_lt : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R}, p.degree = q.degree → p ≠ 0 → p.leadingCoeff = q.leadingCoeff → (p - q).degree < p.degree The theorem `Polynomial.degree_sub_lt` states that for any ring `R` and any two polynomials `p` and `q` over `R`, if the degree of `p` and `q` are equal, and `p` is not the zero polynomial, and the leading coefficients of `p` and `q` are also equal, then the degree of the polynomial resulting from subtracting `q` from `p` (denoted `p - q`) is strictly less than the degree of `p`. In other words, the highest power of `X` in `p - q` is less than the highest power of `X` in `p`. More concisely: Given polynomials `p` and `q` over a ring `R` with equal degrees and non-zero leading coefficients, `p - q` has degree strictly less than that of `p`.
`Polynomial.monic_X` theorem Polynomial.monic_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.Monic This theorem states that the polynomial variable, often referred to as the indeterminate and denoted by `X`, is `Monic` in any semiring `R`. In other words, the leading coefficient of the polynomial `X` is 1. A `Monic` polynomial is defined as a polynomial whose leading coefficient is 1. A semiring is a mathematical structure which is an algebraic structure similar to a ring, but without the requirement that each element must have an additive inverse. More concisely: In any semiring, the polynomial in the indeterminate `X` is monic, meaning its leading coefficient equals 1.
`Polynomial.natDegree_pos_iff_degree_pos` theorem Polynomial.natDegree_pos_iff_degree_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree ↔ 0 < p.degree The theorem `Polynomial.natDegree_pos_iff_degree_pos` states that for any type `R` with a semiring structure and any polynomial `p` over `R`, the natural degree of `p` is greater than 0 if and only if the degree of `p` (which can potentially be an element of the `WithBot ℕ` type) is greater than 0. In other words, a polynomial has a positive natural degree if and only if it has a positive degree, where the degree of a polynomial is defined as the highest power of `X` that appears in the polynomial (or `⊥` for the zero polynomial) and the natural degree forces the degree of the zero polynomial to be 0. More concisely: For any polynomial p over a semiring R, the natural degree is strictly positive if and only if the degree is positive (or non-zero).
`Polynomial.degree_one` theorem Polynomial.degree_one : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.degree 1 = 0 The theorem `Polynomial.degree_one` asserts that for any type `R` that has a structure of a semiring and is nontrivial, the degree of the constant polynomial `1` is `0`. In other words, in a nontrivial semiring, the highest power of `X` that appears in the constant polynomial `1` is `0`. More concisely: In a nontrivial semiring, the constant polynomial 1 has degree 0.
`Polynomial.leadingCoeff_X_sub_C` theorem Polynomial.leadingCoeff_X_sub_C : ∀ {S : Type v} [inst : Ring S] (r : S), (Polynomial.X - Polynomial.C r).leadingCoeff = 1 This theorem states that for any ring `S` and any element `r` of `S`, the leading coefficient of the polynomial `Polynomial.X - Polynomial.C r` is `1`. In other words, if we subtract a constant polynomial `r` from the polynomial variable `X`, the coefficient of the highest power term in the resulting polynomial is always `1`, regardless of the specific ring we are working in or the value of `r`. More concisely: For any ring `S` and element `r` in `S`, the leading coefficient of `Polynomial.X - Polynomial.const r` is `1`.
`Polynomial.leadingCoeff_add_of_degree_lt` theorem Polynomial.leadingCoeff_add_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).leadingCoeff = q.leadingCoeff The theorem `Polynomial.leadingCoeff_add_of_degree_lt` states that for any semiring `R` and any two polynomials `p` and `q` over `R`, if the degree of `p` is less than the degree of `q`, then the leading coefficient of the sum of `p` and `q` is the same as the leading coefficient of `q`. In other words, when adding two polynomials, if one polynomial has a lower degree than the other, the leading coefficient of the result is not affected by the lower degree polynomial. More concisely: If `p` and `q` are polynomials over a semiring `R` with `deg p < deg q`, then the leading coefficient of `p + q` equals the leading coefficient of `q`.
`Polynomial.monic_X_pow` theorem Polynomial.monic_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).Monic The theorem `Polynomial.monic_X_pow` states that for any semiring `R` and for any natural number `n`, the polynomial obtained by raising the polynomial variable `X` to the power `n` is monic. In other words, the leading coefficient of the polynomial `X^n` is 1. A semiring is a type `R` that satisfies certain algebraic properties, including the presence of two binary operations (typically addition and multiplication). More concisely: For any semiring R and natural number n, the polynomial X^n is monic (has a leading coefficient of 1).

LeanAide GPT-4 documentation

Module: Mathlib.Algebra.Polynomial.Degree.Definitions

Polynomial.sum_over_range'

theorem Polynomial.sum_over_range' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S}, (∀ (n : ℕ), f n 0 = 0) → ∀ (n : ℕ), p.natDegree < n → p.sum f = (Finset.range n).sum fun a => f a (p.coeff a)

Polynomial.Monic.coeff_natDegree

theorem Polynomial.Monic.coeff_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.coeff p.natDegree = 1

Polynomial.natDegree_neg

theorem Polynomial.natDegree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).natDegree = p.natDegree := by sorry

Polynomial.leadingCoeff_X_add_C

theorem Polynomial.leadingCoeff_X_add_C : ∀ {S : Type v} [inst : Semiring S] (r : S), (Polynomial.X + Polynomial.C r).leadingCoeff = 1

Polynomial.leadingCoeff_monic_mul

theorem Polynomial.leadingCoeff_monic_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → (p * q).leadingCoeff = q.leadingCoeff

Polynomial.natDegree_X_pow

theorem Polynomial.natDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R] (n : ℕ), (Polynomial.X ^ n).natDegree = n

Polynomial.degree_add_le_of_degree_le

theorem Polynomial.degree_add_le_of_degree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ}, p.degree ≤ ↑n → q.degree ≤ ↑n → (p + q).degree ≤ ↑n

Polynomial.leadingCoeff_ne_zero

theorem Polynomial.leadingCoeff_ne_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.leadingCoeff ≠ 0 ↔ p ≠ 0

Polynomial.natDegree_mul_le

theorem Polynomial.natDegree_mul_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (p * q).natDegree ≤ p.natDegree + q.natDegree

Polynomial.natDegree_add_eq_left_of_natDegree_lt

theorem Polynomial.natDegree_add_eq_left_of_natDegree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.natDegree < p.natDegree → (p + q).natDegree = p.natDegree

Polynomial.natDegree_pow_le

theorem Polynomial.natDegree_pow_le : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, (p ^ n).natDegree ≤ n * p.natDegree

Polynomial.degree_mul

theorem Polynomial.degree_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R] {p q : Polynomial R}, (p * q).degree = p.degree + q.degree

Polynomial.natDegree_X

theorem Polynomial.natDegree_X : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.X.natDegree = 1

Polynomial.natDegree_X_pow_add_C

theorem Polynomial.natDegree_X_pow_add_C : ∀ {R : Type u} [inst : Nontrivial R] [inst : Semiring R] {n : ℕ} {r : R}, (Polynomial.X ^ n + Polynomial.C r).natDegree = n

Polynomial.nextCoeff_of_natDegree_pos

theorem Polynomial.nextCoeff_of_natDegree_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 < p.natDegree → p.nextCoeff = p.coeff (p.natDegree - 1)

Polynomial.natDegree_of_subsingleton

theorem Polynomial.natDegree_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [inst_1 : Subsingleton R], p.natDegree = 0

Polynomial.leadingCoeff_C

theorem Polynomial.leadingCoeff_C : ∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).leadingCoeff = a := by sorry

Polynomial.degree_le_iff_coeff_zero

theorem Polynomial.degree_le_iff_coeff_zero : ∀ {R : Type u} [inst : Semiring R] (f : Polynomial R) (n : WithBot ℕ), f.degree ≤ n ↔ ∀ (m : ℕ), n < ↑m → f.coeff m = 0

Polynomial.natDegree_C_mul_X_pow

theorem Polynomial.natDegree_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), a ≠ 0 → (Polynomial.C a * Polynomial.X ^ n).natDegree = n := by sorry

Polynomial.natDegree_X_pow_sub_C

theorem Polynomial.natDegree_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] [inst_1 : Nontrivial R] {n : ℕ} {r : R}, (Polynomial.X ^ n - Polynomial.C r).natDegree = n

Polynomial.degree_smul_le

theorem Polynomial.degree_smul_le : ∀ {R : Type u} [inst : Semiring R] (a : R) (p : Polynomial R), (a • p).degree ≤ p.degree

Polynomial.degree_X

theorem Polynomial.degree_X : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Nontrivial R], Polynomial.X.degree = 1 := by sorry

Polynomial.natDegree_eq_zero_iff_degree_le_zero

theorem Polynomial.natDegree_eq_zero_iff_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 ↔ p.degree ≤ 0

Polynomial.zero_le_degree_iff

theorem Polynomial.zero_le_degree_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, 0 ≤ p.degree ↔ p ≠ 0

Polynomial.le_natDegree_of_mem_supp

theorem Polynomial.le_natDegree_of_mem_supp : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, ∀ a ∈ p.support, a ≤ p.natDegree

Polynomial.eq_C_of_degree_le_zero

theorem Polynomial.eq_C_of_degree_le_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ 0 → p = Polynomial.C (p.coeff 0)

Polynomial.as_sum_range

theorem Polynomial.as_sum_range : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = (Finset.range (p.natDegree + 1)).sum fun i => (Polynomial.monomial i) (p.coeff i)

Polynomial.natDegree_X_add_C

theorem Polynomial.natDegree_X_add_C : ∀ {R : Type u} [inst : Nontrivial R] [inst : Semiring R] (x : R), (Polynomial.X + Polynomial.C x).natDegree = 1

Polynomial.eq_C_of_natDegree_eq_zero

theorem Polynomial.eq_C_of_natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 → p = Polynomial.C (p.coeff 0)

Polynomial.leadingCoeff_mul'

theorem Polynomial.leadingCoeff_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff

Polynomial.degree_C_le

theorem Polynomial.degree_C_le : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).degree ≤ 0

Polynomial.degree_linear_le

theorem Polynomial.degree_linear_le : ∀ {R : Type u} {a b : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1 := by sorry

Polynomial.eq_C_of_degree_eq_zero

theorem Polynomial.eq_C_of_degree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree = 0 → p = Polynomial.C (p.coeff 0)

Polynomial.Monic.leadingCoeff

theorem Polynomial.Monic.leadingCoeff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.Monic → p.leadingCoeff = 1

Polynomial.natDegree_lt_natDegree_iff

theorem Polynomial.natDegree_lt_natDegree_iff : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p ≠ 0 → (p.natDegree < q.natDegree ↔ p.degree < q.degree)

Polynomial.leadingCoeff_zero

theorem Polynomial.leadingCoeff_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.leadingCoeff 0 = 0

Polynomial.leadingCoeff_X_pow

theorem Polynomial.leadingCoeff_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).leadingCoeff = 1

Polynomial.coeff_eq_zero_of_degree_lt

theorem Polynomial.coeff_eq_zero_of_degree_lt : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.degree < ↑n → p.coeff n = 0

Polynomial.leadingCoeff_mul_monic

theorem Polynomial.leadingCoeff_mul_monic : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.Monic → (p * q).leadingCoeff = p.leadingCoeff

`Polynomial.sum_over_range'`

`Polynomial.Monic.coeff_natDegree`

`Polynomial.natDegree_neg`

`Polynomial.leadingCoeff_X_add_C`

`Polynomial.leadingCoeff_monic_mul`

`Polynomial.natDegree_X_pow`

`Polynomial.degree_add_le_of_degree_le`

`Polynomial.leadingCoeff_ne_zero`

`Polynomial.natDegree_mul_le`

`Polynomial.natDegree_add_eq_left_of_natDegree_lt`

`Polynomial.natDegree_pow_le`

`Polynomial.degree_mul`

`Polynomial.natDegree_X`

`Polynomial.natDegree_X_pow_add_C`

`Polynomial.nextCoeff_of_natDegree_pos`

`Polynomial.natDegree_of_subsingleton`

`Polynomial.leadingCoeff_C`

`Polynomial.degree_le_iff_coeff_zero`

`Polynomial.natDegree_C_mul_X_pow`

`Polynomial.natDegree_X_pow_sub_C`

`Polynomial.degree_smul_le`

`Polynomial.degree_X`

`Polynomial.natDegree_eq_zero_iff_degree_le_zero`

`Polynomial.zero_le_degree_iff`

`Polynomial.le_natDegree_of_mem_supp`

`Polynomial.eq_C_of_degree_le_zero`

`Polynomial.as_sum_range`

`Polynomial.natDegree_X_add_C`

`Polynomial.eq_C_of_natDegree_eq_zero`

`Polynomial.leadingCoeff_mul'`

`Polynomial.degree_C_le`

`Polynomial.degree_linear_le`

`Polynomial.eq_C_of_degree_eq_zero`

`Polynomial.Monic.leadingCoeff`

`Polynomial.natDegree_lt_natDegree_iff`

`Polynomial.leadingCoeff_zero`

`Polynomial.leadingCoeff_X_pow`

`Polynomial.coeff_eq_zero_of_degree_lt`

`Polynomial.leadingCoeff_mul_monic`

`Polynomial.natDegree_le_iff_degree_le`

`Polynomial.degree_le_natDegree`

`Polynomial.natDegree_mem_support_of_nonzero`

`Polynomial.degree_X_pow_sub_C`

`Polynomial.ne_zero_of_natDegree_gt`

`Polynomial.degree_zero`

`Polynomial.X_pow_sub_C_ne_zero`

`Polynomial.degree_mul'`

`Polynomial.degree_add_eq_right_of_degree_lt`

`Polynomial.Monic.ne_zero`

`Polynomial.degree_quadratic_le`

`Polynomial.leadingCoeff_X_pow_add_C`

`Polynomial.natDegree_X_sub_C`

`Polynomial.natDegree_le_of_degree_le`

`Polynomial.natDegree_C_mul_X`

`Polynomial.coeff_eq_zero_of_natDegree_lt`

`Polynomial.natDegree_mul'`

`Polynomial.degree_lt_wf`

`Polynomial.natDegree_sub_C`

`Polynomial.degree_eq_bot`

`Polynomial.degree_mul_le`

`Polynomial.nonempty_support_iff`

`Polynomial.natDegree_monomial`

`Polynomial.degree_neg`

`Polynomial.degree_X_pow_le`

`Polynomial.degree_lt_iff_coeff_zero`

`Polynomial.natDegree_eq_of_degree_eq`

`Polynomial.degree_eq_iff_natDegree_eq`

`Polynomial.natDegree_le_natDegree`

`Polynomial.X_sub_C_ne_zero`

`Polynomial.degree_add_eq_left_of_degree_lt`

`Polynomial.leadingCoeff_C_mul_X_pow`

`Polynomial.degree_X_pow_add_C`

`Polynomial.ne_zero_of_degree_gt`

`Polynomial.degree_add_le`