MvPolynomial.vars_def
theorem MvPolynomial.vars_def :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p : MvPolynomial σ R),
p.vars = p.degrees.toFinset
This theorem states that for any multivariate polynomial `p` over a commutative semiring `R` with variables indexed by `σ`, the set of variables appearing in `p` is exactly the set obtained by removing duplicates from the multiset of maximal degrees of each variable in `p`. This assumes that equality between variables is decidable. In mathematical terms, if we denote by `vars(p)` the set of variables in `p` and `degrees(p)` the multiset of maximal degrees of each variable in `p`, then `vars(p)` is equal to the set obtained from `degrees(p)` by deleting duplicates.
More concisely: For any multivariate polynomial `p` over a commutative semiring `R` with decidable variable equality, the set of variables in `p` equals the multiset of maximal degrees of each variable in `p`, without duplicates.
|
MvPolynomial.vars_prod
theorem MvPolynomial.vars_prod :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} [inst_1 : DecidableEq σ] {s : Finset ι}
(f : ι → MvPolynomial σ R), (s.prod fun i => f i).vars ⊆ s.biUnion fun i => (f i).vars
The theorem `MvPolynomial.vars_prod` states that for any commutative semiring `R`, any type `σ`, any type `ι`, any decidable equality on `σ`, any `Finset` `s` of elements of type `ι`, and any function `f` from `ι` to multivariate polynomials over `σ` and `R`, the set of variables of the product of the family of polynomials given by `f` over the elements of `s` is a subset of the union of the sets of variables of each polynomial in the family. In other words, no new variables are introduced by taking the product of a family of polynomials.
More concisely: For any commutative semiring R, type σ, type ι with decidable equality, Finset s of ι, and function f from ι to multivariate polynomials over σ and R, the set of variables in the product of the polynomials given by f over s is included in the union of the sets of variables of each polynomial in the family.
|
MvPolynomial.vars_mul
theorem MvPolynomial.vars_mul :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (φ ψ : MvPolynomial σ R),
(φ * ψ).vars ⊆ φ.vars ∪ ψ.vars
This theorem states that for any commutative semiring `R` and any type `σ` with decidable equality, and any two multivariate polynomials `φ` and `ψ` over `σ` with coefficients in `R`, the set of variables appearing in the product of `φ` and `ψ` is a subset of the union of the set of variables appearing in `φ` and the set of variables appearing in `ψ`. In other words, multiplication of multivariate polynomials does not introduce any new variables beyond those already present in the factors.
More concisely: For any commutative semiring `R` and type `σ` with decidable equality, if `φ` and `ψ` are multivariate polynomials over `σ` with coefficients in `R`, then the set of variables in the product `φ ⊤ ψ` is included in the union of the sets of variables in `φ` and `ψ`.
|
MvPolynomial.vars_sum_subset
theorem MvPolynomial.vars_sum_subset :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R)
[inst_1 : DecidableEq σ], (t.sum fun i => φ i).vars ⊆ t.biUnion fun i => (φ i).vars
The theorem `MvPolynomial.vars_sum_subset` states that for any commutative semiring `R`, any type `σ`, any finite set `t` of indices `ι`, and any function `φ` that maps each index `ι` to a multivariate polynomial with variables from `σ` and coefficients from `R`, the set of variables that appear in the sum of the polynomials `φ i` for all `i` in `t` is a subset of the union of the sets of variables that appear in each `φ i` individually. Here, the "sum" of a set of polynomials is defined as the result of adding them together, and "union" of a set of sets of variables is defined as the set of all variables that appear in at least one of the sets. The theorem assumes that equality between variables in `σ` is decidable.
More concisely: For any commutative semiring R, type σ, finite set ι, and function φ mapping each index ι to a multivariate polynomial with variables from σ and coefficients from R, the set of variables appearing in the sum of polynomials φ i for all i in ι is a subset of the union of the sets of variables appearing in each φ i. (Assuming decidable equality between variables in σ.)
|
MvPolynomial.vars_C
theorem MvPolynomial.vars_C :
∀ {R : Type u} {σ : Type u_1} {r : R} [inst : CommSemiring R], (MvPolynomial.C r).vars = ∅
The theorem `MvPolynomial.vars_C` asserts that for any type `R`, any type `σ`, and any element `r` of `R`, under the condition that `R` is a commutative semiring, the set of variables appearing in the constant multivariate polynomial with value `r` (`MvPolynomial.C r`) is the empty set. In other words, a constant polynomial doesn't contain any variables.
More concisely: For any commutative semiring `R`, the constant multivariate polynomial `MvPolynomial.C r` over `R` has an empty set of variables.
|
MvPolynomial.vars_monomial
theorem MvPolynomial.vars_monomial :
∀ {R : Type u} {σ : Type u_1} {r : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
r ≠ 0 → ((MvPolynomial.monomial s) r).vars = s.support
The theorem `MvPolynomial.vars_monomial` states that for any commutative semiring `R`, a mapping `σ` of natural numbers, and a non-zero element `r` of `R`, the set of variables appearing in the monomial generated by applying `r` to the monomial function defined by `s` is equal to the support of `s`. Here, the support of a function `s` from `σ` to natural numbers is the set of `σ` for which `s` is nonzero. This essentially means that the variables appearing in such a monomial are precisely those with non-zero exponents.
More concisely: The set of variables in the monomial generated by multiplying a non-zero element with a monomial function equals the support of the function.
|
MvPolynomial.vars_rename
theorem MvPolynomial.vars_rename :
∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] [inst_1 : DecidableEq τ] (f : σ → τ)
(φ : MvPolynomial σ R), ((MvPolynomial.rename f) φ).vars ⊆ Finset.image f φ.vars
This theorem `MvPolynomial.vars_rename` states that for any commutative semiring `R`, any types `σ` and `τ` where `τ` has decidable equality, and any function `f` from `σ` to `τ`, if `φ` is a multivariate polynomial over `σ` and `R`, then the set of variables appearing in the polynomial obtained by renaming the variables of `φ` using `f` is a subset of the image of the set of variables of `φ` under `f`. In other words, if we rename the variables in a polynomial, the new variables are exactly the images under `f` of the original variables.
More concisely: For any commutative semiring R, type σ with decidable equality, function f from σ to type τ, and multivariate polynomial φ over σ and R, the variables in the polynomial obtained by renaming using f are a subset of the image of the polynomial's variables under f.
|
MvPolynomial.hom_congr_vars
theorem MvPolynomial.hom_congr_vars :
∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S]
{f₁ f₂ : MvPolynomial σ R →+* S} {p₁ p₂ : MvPolynomial σ R},
f₁.comp MvPolynomial.C = f₂.comp MvPolynomial.C →
(∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (MvPolynomial.X i) = f₂ (MvPolynomial.X i)) → p₁ = p₂ → f₁ p₁ = f₂ p₂
The theorem `MvPolynomial.hom_congr_vars` states that for a given commutative semiring `R` and another commutative semiring `S`, and for any `σ` indexing the variables of the multivariate polynomial, if `f₁` and `f₂` are ring homomorphisms from the multivariate polynomial ring over `R` into `S`, and `p₁` and `p₂` are polynomials, then the image of `p₁` under `f₁` is equal to the image of `p₂` under `f₂` if and only if three conditions are met: 1) the polynomials `p₁` and `p₂` are equal, 2) `f₁` and `f₂` are equal when mapped over the constant polynomials, and 3) for each variable in the polynomials `p₁` and `p₂`, `f₁` and `f₂` are equal when mapped over the degree `1` monomial of that variable.
More concisely: Given commutative semirings R and S, ring homomorphisms f₁ and f₂ from the multivariate polynomial ring over R into S, and polynomials p₁ and p₂, if p₁ = p₂ and f₁(C) = f₂(C) for all constant polynomials C, and for each variable x, f₁(x) = f₂(x) raised to degree 1, then f₁(p₁) = f₂(p₂).
|