MvPolynomial.degreeOf_def
theorem MvPolynomial.degreeOf_def :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (n : σ) (p : MvPolynomial σ R),
MvPolynomial.degreeOf n p = Multiset.count n p.degrees
The theorem `MvPolynomial.degreeOf_def` states that for any commutative semiring `R`, any type `σ`, any element `n` of type `σ`, and any multivariate polynomial `p` with variables of type `σ` and coefficients in `R`, the degree of the variable `n` in `p` is equal to the count of `n` in the multiset of degrees of `p`. In mathematical terms, if `p` is a multivariate polynomial over a commutative semiring, the highest degree of a variable `n` in `p` is the same as the multiplicity of `n` in the multiset of all degrees of `p`.
More concisely: For any multivariate polynomial `p` over a commutative semiring, the degree of a variable `n` in `p` equals the multiplicity of `n` in the multiset of degrees of `p`.
|
MvPolynomial.degrees_add
theorem MvPolynomial.degrees_add :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
(p + q).degrees ≤ p.degrees ⊔ q.degrees
The theorem `MvPolynomial.degrees_add` states that, for any commutative semiring `R` and any type `σ` with decidable equality, and for any two multivariate polynomials `p` and `q` over `σ` with coefficients in `R`, the degrees of the polynomial formed by adding `p` and `q` is less than or equal to the join (supremum) of the degrees of `p` and `q`. In other words, adding two multivariate polynomials doesn't increase the degree beyond the maximum degree of the two original polynomials.
More concisely: For any commutative semiring R and type σ with decidable equality, the degrees of the sum of two multivariate polynomials over σ with coefficients in R is less than or equal to the maximum of their degrees.
|
MvPolynomial.degrees_monomial
theorem MvPolynomial.degrees_monomial :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (a : R),
((MvPolynomial.monomial s) a).degrees ≤ Finsupp.toMultiset s
The theorem `MvPolynomial.degrees_monomial` states that for any commutative semiring `R`, any type `σ`, any function `s` from `σ` to the natural numbers, and any element `a` of `R`, the multiset of degrees of the monomial formed by applying the function `MvPolynomial.monomial` to `s` and `a` is less than or equal to the multiset obtained from `s` by `Finsupp.toMultiset`. In simpler terms, in a multivariate polynomial, the degrees of any monomial won't exceed the corresponding degrees given by the function `s`.
More concisely: For any commutative semiring R, function s from σ to Nat, and a in R, the degrees of monomials obtained from applying MvPolynomial.monomial to s and a are less than or equal to the multiset obtained from s using Finsupp.toMultiset.
|
MvPolynomial.totalDegree_add
theorem MvPolynomial.totalDegree_add :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a b : MvPolynomial σ R),
(a + b).totalDegree ≤ max a.totalDegree b.totalDegree
The theorem `MvPolynomial.totalDegree_add` states that for any commutative semiring `R`, and any set of variables indices `σ`, the total degree of the sum of two multivariate polynomials `a` and `b` (from `R` over `σ`) is less than or equal to the maximum of their respective total degrees.
Here, the total degree of a multivariate polynomial is defined as the maximum sum of exponents in all of its monomials. The theorem is essentially saying that adding two multivariate polynomials doesn't increase the degree beyond the degree of the polynomial with the highest degree in the addends.
More concisely: The total degree of the sum of two multivariate polynomials over a commutative semiring is less than or equal to the maximum of their individual total degrees.
|
MvPolynomial.totalDegree_C
theorem MvPolynomial.totalDegree_C :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R), (MvPolynomial.C a).totalDegree = 0
This theorem states that for any type `R` and `σ`, with `R` being a commutative semiring, the total degree of a constant multivariate polynomial is zero. In more detail, given any element `a` from `R`, when we construct a constant polynomial with value `a` using `MvPolynomial.C`, the maximum absolute degree of its monomials, as calculated by `MvPolynomial.totalDegree`, is always zero.
More concisely: For any commutative semiring `R` and constant polynomial `p` of type `MvPolynomial R` with `p = MvPolynomial.C a` for some `a : R`, the total degree of `p` is zero.
|
MvPolynomial.degrees_zero
theorem MvPolynomial.degrees_zero : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.degrees 0 = 0
This theorem states that for any commutative semiring `R` and any type `σ`, the degrees of the zero polynomial (which is a multi-variable polynomial over `R` with variables from `σ`) is zero. In other words, there are no terms in this polynomial, so there are no variables with any associated degree.
More concisely: For any commutative semiring R and type σ, the zero polynomial over R with variables from σ has degree 0.
|
MvPolynomial.degreeOf_eq_sup
theorem MvPolynomial.degreeOf_eq_sup :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ) (f : MvPolynomial σ R),
MvPolynomial.degreeOf n f = f.support.sup fun m => m n
The theorem `MvPolynomial.degreeOf_eq_sup` states that for any commutative semiring `R`, any type `σ`, any instance of that semiring, any element `n` of type `σ`, and any multivariate polynomial `f` with coefficients in `R` and variables indexed by `σ`, the highest power of the variable indexed by `n` that appears in the polynomial `f` (`MvPolynomial.degreeOf n f`) is equal to the supremum (maximum) value obtained by applying a function to each element of the finite set of all `m : σ →₀ ℕ` (a map from `σ` to `ℕ` where only finitely many `σ` are non-zero) such that `X^m` has a non-zero coefficient in the polynomial `f` (`MvPolynomial.support f`), where the function takes such an `m` to its `n`-th component. In other words, the maximum degree of a particular variable `n` in a multivariate polynomial `f` is achieved at the monomial in `f` where the power of `n` is the highest.
More concisely: For any commutative semiring R, multivariate polynomial f with coefficients in R, and variable n of type σ, the degree of n in f is equal to the maximum value of the component m(n) of maps m: σ →₀ ℕ such that X^m is a non-zero term in f.
|
MvPolynomial.le_totalDegree
theorem MvPolynomial.le_totalDegree :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : σ →₀ ℕ},
s ∈ p.support → (s.sum fun x e => e) ≤ p.totalDegree
The `MvPolynomial.le_totalDegree` theorem states that for any multivariate polynomial `p` over a commutative semiring `R` with variables indexed by set `σ`, and any monomial `s` in the support of `p` (i.e., a monomial with a non-zero coefficient in `p`), the sum of the exponents in the monomial `s` is less than or equal to the total degree of the polynomial `p`. The total degree of a multivariate polynomial is defined as the maximum sum of the exponents over all its monomials.
More concisely: For any multivariate polynomial `p` over a commutative semiring `R` with variables indexed by set `σ`, the degree of each monomial `s` in the support of `p` is less than or equal to the total degree of `p`.
|
MvPolynomial.degrees_C
theorem MvPolynomial.degrees_C :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R), (MvPolynomial.C a).degrees = 0
This theorem states that for any type `R` and `σ`, with `R` being a commutative semiring, and for any element `a` of `R`, the multiset of degrees of the constant polynomial with value `a` is zero. In other words, a constant polynomial has no variables to have degrees of, so the multiset of degrees is empty, which is represented by `0` in this context.
More concisely: For any commutative semiring `R` and its element `a`, the multiset of degrees of the constant polynomial `λ x : R, a` is the empty multiset.
|
MvPolynomial.degrees_def
theorem MvPolynomial.degrees_def :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R),
p.degrees = p.support.sup fun s => Finsupp.toMultiset s
The theorem `MvPolynomial.degrees_def` states that for any commutative semiring `R`, any type `σ`, and any instance of decidable equality on `σ`, for any multivariate polynomial `p` with coefficients in `R` and variables indexed by `σ`, the degrees of `p` (defined as the maximal degrees of each variable, expressed as a multiset) is equal to the supremum (greatest element) of the multiset conversion of the finite set of all monomials `m : σ →₀ ℕ` in `p` that have non-zero coefficients. This multiset is obtained by taking each monomial in the polynomial's support and converting it to a multiset where each variable appears a number of times equal to its exponent in the monomial.
More concisely: The degrees of a multivariate polynomial with coefficients in a commutative semiring and decidable equality on its index type is equal to the multiset of monomial degrees in the polynomial, where each monomial is counted by its highest variable exponent.
|