MvPolynomial.coeff_homogeneousComponent
theorem MvPolynomial.coeff_homogeneousComponent :
∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (n : ℕ) (φ : MvPolynomial σ R) (d : σ →₀ ℕ),
MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent n) φ) =
if MvPolynomial.degree d = n then MvPolynomial.coeff d φ else 0
This theorem states that for any commutative semiring `R`, any natural number `n`, any multivariate polynomial `φ` over the semiring `R` with variables indexed by `σ`, and any function `d` from `σ` to the natural numbers, the coefficient of the monomial `d` in the `n`-th homogeneous component of `φ` equals the coefficient of `d` in `φ` if the sum of the values of `d` over its support equals `n`; otherwise, this coefficient is zero. Essentially, it is examining the coefficient of a certain monomial in a particular homogeneous component of a multivariate polynomial.
More concisely: For any commutative semiring `R`, any multivariate polynomial `φ` over `R`, and any natural number `n`, the coefficient of a monomial with a sum of exponents equal to `n` in `φ`'s `n`-th homogeneous component equals the coefficient of that monomial in `φ`, otherwise it is zero.
|
MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
theorem MvPolynomial.homogeneousSubmodule_eq_finsupp_supported :
∀ (σ : Type u_1) (R : Type u_3) [inst : CommSemiring R] (n : ℕ),
MvPolynomial.homogeneousSubmodule σ R n = Finsupp.supported R R {d | MvPolynomial.degree d = n}
This theorem states that, for any type `σ`, type `R` with a commutative semiring structure, and natural number `n`, the submodule of homogeneous multivariate polynomials of degree `n` is equal to the submodule of finitely supported functions whose support is contained in the set of functions `d` for which the degree of the monomial is `n`. In other words, the homogeneous submodule of degree `n` multivariate polynomials is exactly the submodule supported on monomials of degree `n`. This is important because even though these two modules are equal, the former definition allows for a more convenient computational reduction.
More concisely: The submodule of homogeneous multivariate polynomials of degree n equals the submodule of finitely supported functions whose support consists of monomials of degree n.
|
MvPolynomial.isHomogeneous_X
theorem MvPolynomial.isHomogeneous_X :
∀ {σ : Type u_1} (R : Type u_3) [inst : CommSemiring R] (i : σ), (MvPolynomial.X i).IsHomogeneous 1
This theorem states that for any type `σ` and any ring `R` that is a commutative semiring, for any `i` of type `σ`, the polynomial `MvPolynomial.X i` is homogeneous of degree 1. In other words, all the monomials in the polynomial `MvPolynomial.X i` have degree 1. In the context of multivariate polynomials, `MvPolynomial.X i` refers to the degree `1` monomial $X_i$, and a multivariate polynomial is considered homogeneous of a certain degree if all monomials that compose it have that same degree.
More concisely: For any commutative semiring R and type σ, the polynomial Map (MvPolynomial.X) i is a homogeneous polynomial of degree 1, where MvPolynomial.X i is the degree 1 monomial with respect to the variable i in multivariate polynomials.
|
MvPolynomial.isHomogeneous_C
theorem MvPolynomial.isHomogeneous_C :
∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R] (r : R), (MvPolynomial.C r).IsHomogeneous 0
The theorem `MvPolynomial.isHomogeneous_C` states that for any type `σ`, a commutative semiring `R` and any element `r` of `R`, the constant polynomial with value `r` is homogeneous of degree 0. In mathematical terms, this means that every monomial in the polynomial has degree 0, i.e., it is a constant term.
More concisely: The constant polynomial is a homogeneous polynomial of degree 0.
|
MvPolynomial.isHomogeneous_monomial
theorem MvPolynomial.isHomogeneous_monomial :
∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {d : σ →₀ ℕ} (r : R) {n : ℕ},
MvPolynomial.degree d = n → ((MvPolynomial.monomial d) r).IsHomogeneous n
The theorem `MvPolynomial.isHomogeneous_monomial` states that for any type `σ`, any type `R` with a commutative semiring structure, any function `d` from `σ` to natural numbers, any element `r` of `R`, and any natural number `n`, if the sum of the outputs of `d` over its support equals `n`, then the multivariate polynomial which is the monomial with coefficient `r` and exponents given by `d` is homogeneous of degree `n`. In simpler terms, this theorem guarantees that a monomial of a multivariate polynomial is of homogeneous degree `n` if the sum of its exponents equals `n`.
More concisely: Given a commutative semiring R, a function d from σ to natural numbers with sum of outputs equal to n over its support, and r an element of R, the monomial x^d with coefficient r is a homogeneous multivariate polynomial of degree n.
|