Polynomial.natTrailingDegree_zero
theorem Polynomial.natTrailingDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.natTrailingDegree 0 = 0 := by
sorry
The theorem `Polynomial.natTrailingDegree_zero` states that for any type `R` equipped with a structure of a semiring, the natural trailing degree of the zero polynomial is zero. In the context of polynomial mathematics, the trailing degree is the smallest degree of a polynomial's non-zero terms. Hence, this theorem is essentially saying that the smallest degree of non-zero terms of a zero polynomial (which has no non-zero terms) is considered to be zero.
More concisely: The trailing degree of the zero polynomial in a semiring is zero.
|
Polynomial.trailingDegree_monomial
theorem Polynomial.trailingDegree_monomial :
∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], a ≠ 0 → ((Polynomial.monomial n) a).trailingDegree = ↑n := by
sorry
This theorem states that for any type `R`, any non-zero element `a` of `R`, and any natural number `n` within a semiring `R`, the trailing degree of the polynomial formed by the monomial `a * X^n` is equal to `n`. In other words, in a semiring, the smallest `X`-exponent in the monomial `a * X^n` is `n` when `a` is not zero.
More concisely: In a semiring, the degree of the monomial `a * X^n` with non-zero `a` is equal to the natural number `n`.
|
Polynomial.trailingCoeff_nonzero_iff_nonzero
theorem Polynomial.trailingCoeff_nonzero_iff_nonzero :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingCoeff ≠ 0 ↔ p ≠ 0
This theorem states that for any type `R` that is an instance of the `Semiring` type class and for any polynomial `p` over `R`, the trailing coefficient of `p` is nonzero if and only if `p` itself is nonzero. In other words, a polynomial is nonzero if and only if the coefficient of its smallest power is nonzero.
More concisely: A polynomial over a semiring is nonzero if and only if its leading coefficient is nonzero.
|
Polynomial.natTrailingDegree_le_of_ne_zero
theorem Polynomial.natTrailingDegree_le_of_ne_zero :
∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → p.natTrailingDegree ≤ n
The theorem `Polynomial.natTrailingDegree_le_of_ne_zero` asserts that for any type `R` which forms a semiring, any natural number `n`, and any polynomial `p` over `R`, if the coefficient of `X^n` in `p` is non-zero, then the natural trailing degree of `p` is less than or equal to `n`. The natural trailing degree of a polynomial is defined as the lowest degree of the polynomial's non-zero terms, with a default value of 0 if there is no such term (i.e., in the case of the zero polynomial). Thus, this theorem essentially states that the natural trailing degree of a non-zero polynomial is at most the degree of any term with a non-zero coefficient.
More concisely: For any semiring `R`, natural number `n`, and polynomial `p` over `R` with a non-zero coefficient for `X^n`, the natural trailing degree of `p` is less than or equal to `n`.
|
Polynomial.le_trailingDegree_monomial
theorem Polynomial.le_trailingDegree_monomial :
∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], ↑n ≤ ((Polynomial.monomial n) a).trailingDegree
The theorem `Polynomial.le_trailingDegree_monomial` states that for any type `R`, any element `a` of `R`, and any natural number `n`, if `R` is a semiring, then the natural number `n`, when considered as an element of extended natural numbers, is less than or equal to the trailing degree of the polynomial formed by `a * X^n`. In other words, the smallest power of X that appears in the monomial `a * X^n` is `n` itself, or a lesser power if `a` is zero.
More concisely: For any semiring R, any element a in R, and natural number n, the trailing degree of the polynomial a * X^n is at least n.
|
Polynomial.natTrailingDegree_monomial
theorem Polynomial.natTrailingDegree_monomial :
∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], a ≠ 0 → ((Polynomial.monomial n) a).natTrailingDegree = n := by
sorry
The theorem `Polynomial.natTrailingDegree_monomial` states that for any semiring `R`, and any element `a` of `R` and any natural number `n`, if `a` is not zero, then the trailing degree (calculated as a natural number) of the monomial `a * X^n` (represented by `((Polynomial.monomial n) a)`) is `n`. In other words, the natural trailing degree of a nonzero monomial is equal to the power of `X` in that monomial.
More concisely: The trailing degree of a nonzero monomial `a * X^n` in a semiring equals the natural number `n`.
|
Polynomial.trailingDegree_eq_natTrailingDegree
theorem Polynomial.trailingDegree_eq_natTrailingDegree :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.trailingDegree = ↑p.natTrailingDegree
The theorem `Polynomial.trailingDegree_eq_natTrailingDegree` states that for any non-zero polynomial `p` in a semiring `R`, the trailing degree of `p` is equal to the natural number trailing degree of `p`, when the latter is treated as an element of `ℕ∞` (the set of natural numbers extended with positive infinity). In other words, the smallest exponent of `X` that appears in `p` (which is the trailing degree of `p`) is equal to the forced natural number value of the trailing degree, where we define this forced value to be 0 when the trailing degree is positive infinity.
More concisely: The trailing degree of a non-zero polynomial in a semiring equals the coerced natural number value of its trailing degree in the extended natural numbers.
|
Polynomial.trailingDegree_zero
theorem Polynomial.trailingDegree_zero : ∀ {R : Type u} [inst : Semiring R], Polynomial.trailingDegree 0 = ⊤
The theorem `Polynomial.trailingDegree_zero` states that for any type `R` that forms a semiring, the trailing degree of the zero polynomial equals `⊤`, which can be interpreted as infinity. Here, the trailing degree of a polynomial is defined as the smallest power of `X` that appears in the polynomial. For the zero polynomial, which does not have any terms with `X`, the smallest power of `X` is considered to be infinity.
More concisely: For any semiring type R, the trailing degree of the zero polynomial is infinity.
|
Polynomial.natTrailingDegree_C
theorem Polynomial.natTrailingDegree_C :
∀ {R : Type u} [inst : Semiring R] (a : R), (Polynomial.C a).natTrailingDegree = 0
The theorem `Polynomial.natTrailingDegree_C` states that for any type `R` that forms a semiring (a structure with two binary operations that generalizes the arithmetic operations of addition and multiplication), and any element `a` of this type `R`, the natural trailing degree of the constant polynomial `a` is zero. In other words, when a constant is treated as a polynomial (with coefficients in `R`), its trailing degree (the lowest power of the indeterminate with a non-zero coefficient) is zero.
More concisely: For any semiring `R` and its element `a`, the constant polynomial `a` has trailing degree zero as a polynomial in `R`.
|
Polynomial.trailingCoeff_eq_zero
theorem Polynomial.trailingCoeff_eq_zero :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.trailingCoeff = 0 ↔ p = 0
The theorem `Polynomial.trailingCoeff_eq_zero` states that for any type `R` that is a semiring, and any polynomial `p` with coefficients in `R`, the trailing coefficient of `p` is zero if and only if `p` itself is the zero polynomial. Here, the "trailing coefficient" of a polynomial refers to the coefficient of the smallest power of `X` in the polynomial.
More concisely: For any semiring `R` and polynomial `p` over `R` in the indeterminate `X`, `p.leadingTerm.coeff = 0` if and only if `p` is the zero polynomial.
|
Polynomial.natTrailingDegree_mul
theorem Polynomial.natTrailingDegree_mul :
∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [inst_1 : NoZeroDivisors R],
p ≠ 0 → q ≠ 0 → (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
The theorem `Polynomial.natTrailingDegree_mul` states that for any two non-zero polynomials `p` and `q` over a semiring `R` that has no zero divisors, the natural trailing degree of the product `p * q` is the sum of the natural trailing degrees of `p` and `q`. In other words, when you multiply two non-zero polynomials, the degree of the resulting polynomial is the sum of the degrees of the original polynomials.
More concisely: The natural trailing degrees of the product of two non-zero polynomials over a semiring without zero divisors equals the sum of their natural trailing degrees.
|
Polynomial.natTrailingDegree_le_natDegree
theorem Polynomial.natTrailingDegree_le_natDegree :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p.natTrailingDegree ≤ p.natDegree
The theorem `Polynomial.natTrailingDegree_le_natDegree` states that for any type `R` that is a semiring, and for any polynomial `p` over this type, the natural trailing degree of `p` is less than or equal to its natural degree. In terms of polynomial mathematics, this implies that the lowest degree of a non-zero term in the polynomial is always less than or equal to the highest degree of a term in the polynomial.
More concisely: For any semiring R and polynomial p over R, the degree of the leading term of p is greater than or equal to the degree of any other non-zero term in p. (The theorem in Lean actually states the negative of this, as it defines trailing degree as the negative of the degree of the leading term, hence the inequality is reversed in the Lean theorem.)
|
Polynomial.coeff_eq_zero_of_lt_natTrailingDegree
theorem Polynomial.coeff_eq_zero_of_lt_natTrailingDegree :
∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n < p.natTrailingDegree → p.coeff n = 0
The theorem `Polynomial.coeff_eq_zero_of_lt_natTrailingDegree` states that for any semiring `R`, polynomial `p` over `R`, and natural number `n`, if `n` is less than the natural trailing degree of the polynomial `p`, then the coefficient of `X^n` in `p` is zero. In other words, all coefficients corresponding to powers of `X` that are less than the natural trailing degree of the polynomial are zero.
More concisely: For any semiring R, polynomial p over R in X, and natural number n, if the natural trailing degree of p is greater than n, then the coefficient of X^n in p is zero.
|