MvPolynomial.rename_X
theorem MvPolynomial.rename_X :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (i : σ),
(MvPolynomial.rename f) (MvPolynomial.X i) = MvPolynomial.X (f i)
The theorem `MvPolynomial.rename_X` states that for any commutative semiring `R` and any types `σ` and `τ`, if you have a function `f` that maps values from type `σ` to type `τ`, and an element `i` of type `σ`, then renaming the variables of the degree `1` multivariate polynomial `X_i` using the function `f` yields the degree `1` multivariate polynomial `X_{f(i)}`. In simpler terms, renaming the variable of a degree `1` monomial using a renaming function is equivalent to applying the renaming function to the variable and then constructing the degree `1` monomial.
More concisely: For any commutative semiring `R`, given a function `f : σ → τ` and an element `i : σ`, the degree 1 multivariate polynomial `X_i` with respect to `R` is equal to the degree 1 multivariate polynomial `X_{f(i)}` with respect to `R` obtained by applying the function `f` to the variable name.
|
MvPolynomial.rename_C
theorem MvPolynomial.rename_C :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (r : R),
(MvPolynomial.rename f) (MvPolynomial.C r) = MvPolynomial.C r
The theorem `MvPolynomial.rename_C` states that for any types `σ`, `τ`, and `R` with `R` being a commutative semiring, any function `f` from `σ` to `τ`, and any element `r` of `R`, the act of renaming variables in a constant multivariable polynomial (using the function `MvPolynomial.rename f`) does not change the polynomial. In other words, if we have a constant multivariable polynomial `MvPolynomial.C r` (which is a polynomial with a constant value `r`), renaming its variables using any function `f` will still yield the same constant polynomial `MvPolynomial.C r`.
More concisely: For any commutative semiring `R`, function `f` from type `σ` to type `τ`, and constant polynomial `MvPolynomial.C r` over `R`, the renamed polynomial `MvPolynomial.rename f (MvPolynomial.C r)` is equal to the original constant polynomial `MvPolynomial.C r`.
|
MvPolynomial.rename_id
theorem MvPolynomial.rename_id :
∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R), (MvPolynomial.rename id) p = p := by
sorry
This theorem states that for any multivariate polynomial `p` with variables indexed by the set `σ` and coefficients in a commutative semiring `R`, renaming the variables in `p` by the identity function results in the same polynomial `p`. The identity function here maps each variable to itself. In other words, if we do not change the names of the variables in a multivariate polynomial, the polynomial remains unchanged.
More concisely: For any multivariate polynomial over a commutative semiring, renaming variables by the identity function leaves the polynomial unchanged.
|
MvPolynomial.rename_rename
theorem MvPolynomial.rename_rename :
∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (g : τ → α)
(p : MvPolynomial σ R), (MvPolynomial.rename g) ((MvPolynomial.rename f) p) = (MvPolynomial.rename (g ∘ f)) p
The theorem `MvPolynomial.rename_rename` states that for every commutative semiring `R` and types `σ`, `τ`, and `α`, if you have two renaming functions `f: σ → τ` and `g: τ → α`, and a multivariate polynomial `p` over `σ` and `R`, then applying the renaming function `f` to the polynomial `p` and then applying the renaming function `g` to the result is the same as first composing the functions `g` and `f` to create a new renaming function and then applying this new function to the polynomial `p`. In other words, the process of renaming variables in a multivariate polynomial is associative with respect to function composition.
More concisely: For every commutative semiring `R` and types `σ`, `τ`, and `α`, and given renaming functions `f: σ → τ` and `g: τ → α`, the renaming of a multivariate polynomial `p` over `σ` and `R` via `f` and then via `g` equals the renaming via the composite function `g ∘ f`.
|
MvPolynomial.rename_monomial
theorem MvPolynomial.rename_monomial :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (d : σ →₀ ℕ) (r : R),
(MvPolynomial.rename f) ((MvPolynomial.monomial d) r) = (MvPolynomial.monomial (Finsupp.mapDomain f d)) r
The theorem `MvPolynomial.rename_monomial` states that for any commutative semiring `R`, any function `f` from type `σ` to type `τ`, any finitely supported function `d` from type `σ` to natural numbers, and any element `r` of `R`, the operation of renaming the variables in the monomial given by `d` and `r` in the multivariable polynomial over `R` with variables of type `σ` using `f`, is the same as creating a monomial in the multivariable polynomial over `R` with variables of type `τ` whose exponents are given by the finitely supported function obtained by mapping the domain of `d` using `f`, and whose coefficient is `r`. In other words, renaming the variables in a monomial is equivalent to creating a new monomial with the variables renamed.
More concisely: For any commutative semiring R, function f from type σ to τ, finitely supported function d from type σ to natural numbers, and element r of R, the operation of renaming variables in a multivariable polynomial over R using f and d is equivalent to creating a new monomial with variables from τ and corresponding exponents from the image of d under f, and coefficient r.
|
MvPolynomial.rename_eq
theorem MvPolynomial.rename_eq :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (p : MvPolynomial σ R),
(MvPolynomial.rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
The theorem `MvPolynomial.rename_eq` states that for any commutative semiring `R` and any function `f` from type `σ` to type `τ`, the renaming of all variables in a multivariate polynomial `p` of type `σ` with coefficients in `R` via the function `f` is equivalent to mapping the domain of `p` twice with the function `f`. Here, `MvPolynomial.rename f p` is renaming all variables in `p` according to `f` and `Finsupp.mapDomain (Finsupp.mapDomain f) p` is applying the function `f` to the domain of `p` twice.
More concisely: For any commutative semiring R and function f from type σ to type τ, renaming variables in a multivariate polynomial p of type σ with coefficients in R via f is equivalent to applying f to the domain of p twice.
|
MvPolynomial.exists_fin_rename
theorem MvPolynomial.exists_fin_rename :
∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R),
∃ n f, ∃ (_ : Function.Injective f), ∃ q, p = (MvPolynomial.rename f) q
This theorem states that for every multivariate polynomial `p` over a commutative semiring `R` and an index set `σ`, there exists a finite number `n` and a function `f` such that `f` is injective and there exists another polynomial `q` such that `p` is equal to the result of renaming the variables of `q` according to the function `f`. Essentially, this theorem guarantees that every polynomial can be expressed in terms of a finite number of variables.
More concisely: Every multivariate polynomial over a commutative semiring can be expressed as a renamed variant of a polynomial with a finite number of variables.
|
MvPolynomial.exists_finset_rename
theorem MvPolynomial.exists_finset_rename :
∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R),
∃ s q, p = (MvPolynomial.rename Subtype.val) q
The theorem `MvPolynomial.exists_finset_rename` states that for every multivariate polynomial `p` (where the index set of the variables is of type `σ` and the coefficient ring is `R`), there exists a set `s` and another multivariate polynomial `q` such that `p` can be expressed as the renaming of `q` by mapping each variable to its underlying element in the base type. This theorem essentially says that every multivariate polynomial can be presented in terms of a finite number of variables.
More concisely: For every multivariate polynomial `p` over a ring `R` with index set `σ`, there exists a set `s` and a polynomial `q` such that `p` is the renaming of `q` by mapping each variable to its underlying element in `s`.
|
MvPolynomial.exists_finset_rename₂
theorem MvPolynomial.exists_finset_rename₂ :
∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p₁ p₂ : MvPolynomial σ R),
∃ s q₁ q₂, p₁ = (MvPolynomial.rename Subtype.val) q₁ ∧ p₂ = (MvPolynomial.rename Subtype.val) q₂
The theorem `MvPolynomial.exists_finset_rename₂` states that for any two multivariate polynomials `p₁` and `p₂` in a commutative semiring `R` of possibly infinitely many variables indexed by the set `σ`, there exists a finite subset `s` of `σ` such that both `p₁` and `p₂` can be expressed as polynomials in the semiring `R` of variables indexed by `s`. More specifically, there exist two polynomials `q₁` and `q₂` such that `p₁` and `p₂` are equivalent to `q₁` and `q₂` respectively, after renaming variables using the `Subtype.val` function, which retrieves the underlying element from a subtype.
More concisely: For any multivariate polynomials `p₁` and `p₂` over a commutative semiring `R` with possibly infinitely many variables `σ`, there exists a finite subset `s` of `σ` such that `p₁` and `p₂` are equivalent to polynomials in `R` with variables restricted to `s`.
|