MvPolynomial.coe_monomial
theorem MvPolynomial.coe_monomial :
∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : σ →₀ ℕ) (a : R),
↑((MvPolynomial.monomial n) a) = (MvPowerSeries.monomial R n) a
The theorem `MvPolynomial.coe_monomial` states that for any commutative semiring `R` and for any `n` of type `σ →₀ ℕ` (which refers to a function which maps from a generic type `σ` to non-negative integers) and any `a` of type `R`, the coerced result of applying the multivariate polynomial monomial function `MvPolynomial.monomial` to `n` and `a` equals the result of applying the multivariate power series monomial function `MvPowerSeries.monomial` to `R`, `n` and `a`. Essentially, this theorem establishes a connection between monomials in the context of multivariate polynomials and multivariate power series within a commutative semiring.
More concisely: For any commutative semiring R, function n : σ →₀ ℕ, and element a in R, the coerced result of MvPolynomial.monomial applying to n and a equals the result of MvPowerSeries.monomial applying to R, n, and a.
|
MvPowerSeries.isUnit_constantCoeff
theorem MvPowerSeries.isUnit_constantCoeff :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R),
IsUnit φ → IsUnit ((MvPowerSeries.constantCoeff σ R) φ)
This theorem states that if a multivariate formal power series, denoted as φ, is invertible in the context of a semiring R and a set of variables σ, then its constant coefficient is also invertible. In essence, if the entire power series has a two-sided inverse (meaning it is a "unit" in the algebraic sense), then the same is true for the series' constant term.
More concisely: If a multivariate formal power series φ over semiring R and set of variables σ is invertible, then its constant coefficient is invertible in R.
|
MvPowerSeries.ext
theorem MvPowerSeries.ext :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ ψ : MvPowerSeries σ R},
(∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ) → φ = ψ
The theorem `MvPowerSeries.ext` states that for any semiring `R` and index set `σ`, if two multivariate formal power series `φ` and `ψ` have all their coefficients equal, i.e., for each `n` which is a function from the index set `σ` to non-negative integers, the `n`th coefficient of `φ` equals the `n`th coefficient of `ψ`, then these two power series `φ` and `ψ` are identical. The theorem essentially establishes the principle of coefficient-wise equality for multivariate formal power series over a semiring.
More concisely: If two multivariate formal power series over a semiring have equal coefficients for all monomials, then they are equal.
|
MvPowerSeries.coeff_X
theorem MvPowerSeries.coeff_X :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (s : σ),
(MvPowerSeries.coeff R n) (MvPowerSeries.X s) = if n = fun₀ | s => 1 then 1 else 0
This theorem states that for any semiring `R` and type `σ`, with decidable equality on `σ`, and any given multivariate formal power series coefficient function `n` and a variable `s` of the power series, the `n`th coefficient of the variable `s` in the multivariate formal power series is 1 if `n` matches the function that returns 1 for `s` and 0 otherwise. In other words, it specifies the coefficients of the variables in a multivariate formal power series over a semiring.
More concisely: For any semiring `R` with decidable equality and type `σ`, the multivariate formal power series coefficient function `n` of a variable `s` equals 1 in `R` if `n` is the function that returns 1 for `s`, and 0 otherwise.
|
MvPowerSeries.coeff_mul_monomial
theorem MvPowerSeries.coeff_mul_monomial :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
(MvPowerSeries.coeff R m) (φ * (MvPowerSeries.monomial R n) a) =
if n ≤ m then (MvPowerSeries.coeff R (m - n)) φ * a else 0
This theorem states that for any types `σ` and `R`, and given a semiring instance on `R`, if we have two functions `m` and `n` from `σ` to natural numbers, a multivariate formal power series `φ` over `σ` and `R`, and a coefficient `a` from `R`, then the `m`th coefficient of the product of `φ` and the `n`th monomial with coefficient `a` is equal to the product of the `(m-n)`th coefficient of `φ` and `a` if `n` is less than or equal to `m`, and is zero otherwise. This theorem describes how the coefficients of the product of a multivariate formal power series and a monomial are distributed.
More concisely: For any semiring `R`, type `σ`, and functions `m` and `n` from `σ` to natural numbers, if `φ` is a multivariate formal power series over `σ` and `R`, and `a` is a coefficient from `R`, then the coefficient of the `m`th monomial of `φ * (a * ∏ (x_i ^ n_i))` is `a * (coefficient_m φ)` if `n_i <= m_i` for all `i`, and is zero otherwise.
|
MvPowerSeries.coeff_add_mul_monomial
theorem MvPowerSeries.coeff_add_mul_monomial :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
(MvPowerSeries.coeff R (m + n)) (φ * (MvPowerSeries.monomial R n) a) = (MvPowerSeries.coeff R m) φ * a
This theorem states that for any semiring `R`, index set of variables `σ`, indices `m` and `n`, multivariate formal power series `φ` over the variables `σ` with coefficients from `R` and a coefficient `a` from `R`, the `m + n`th coefficient of the product of `φ` and the `n`th monomial times `a` equals the `m`th coefficient of `φ` times `a`.
Here the product is in the sense of multivariate formal power series, and the `n`th monomial is understood as a multivariate formal power series where only the `n`th coefficient is `a` and all other coefficients are zero. This theorem essentially describes how coefficients are distributed when multiplying a multivariate formal power series by a monomial.
More concisely: For any semiring `R`, multivariate formal power series `φ` over variables `σ` with coefficients from `R`, index `n`, and coefficient `a` from `R`, the `m + n`th coefficient of `a * (φ * ξ^n)` equals `m`th coefficient of `φ * a * ξ^n`, where `ξ` is the standard basis of the free commutative monoid over `σ`.
|
MvPowerSeries.coeff_add_monomial_mul
theorem MvPowerSeries.coeff_add_monomial_mul :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
(MvPowerSeries.coeff R (m + n)) ((MvPowerSeries.monomial R m) a * φ) = a * (MvPowerSeries.coeff R n) φ
This theorem states that for any semiring `R`, any multivariate formal power series `φ` over the index set `σ` and coefficients in `R`, and any `m`, `n` in the set of functions from `σ` to natural numbers and `a` in `R`, the coefficient of the term with exponent `m + n` in the product of the `m`th monomial (with coefficient `a`) and `φ`, is equal to `a` times the `n`th coefficient of `φ`. In mathematical terms, it means that the coefficient of `x^(m + n)` in the multiplication of a monomial `a * x^m` and a power series `φ(x)` is `a` times the coefficient of `x^n` in `φ(x)`.
More concisely: For any semiring `R`, multivariate formal power series `φ` over index set `σ` with coefficients in `R`, and `a` in `R` and functions `m, n : σ -> Nat`, the coefficient of `x^(m + n)` in the product of `a * x^m` and `φ(x)` equals `a * φ^n(x)`, where `φ^n(x)` denotes the `n`th coefficient of `φ(x)` with respect to `x`.
|
MvPowerSeries.coeff_monomial
theorem MvPowerSeries.coeff_monomial :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (m n : σ →₀ ℕ) (a : R),
(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = if m = n then a else 0
The theorem `MvPowerSeries.coeff_monomial` states that for any types `σ` and `R`, where `R` is a semiring and `σ` has decidable equality, for any multivariate indices `m` and `n` (which are functions from `σ` to `ℕ`), and for any element `a` from `R`, the `m`th coefficient of the `n`th monomial of the multivariate formal power series, scaled by `a`, equals `a` if `m` equals `n` and zero otherwise. In other words, it expresses that in a multivariate power series, the coefficient of a particular monomial is the scaling factor if the indices match, and is zero for all other monomials.
More concisely: For any semiring `R` and type `σ` with decidable equality, the `m`th coefficient of the `n`th monomial in a multivariate formal power series over `R` scaled by an element `a` from `R` is equal to `a` if `m` equals `n`, and zero otherwise.
|
MvPowerSeries.algebraMap_apply
theorem MvPowerSeries.algebraMap_apply :
∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
{r : R}, (algebraMap R (MvPowerSeries σ A)) r = (MvPowerSeries.C σ A) ((algebraMap R A) r)
The theorem `MvPowerSeries.algebraMap_apply` states that for any type `σ`, any commutative semiring `R`, any semiring `A`, and any element `r` of `R`, if `A` has an algebra structure over `R`, then applying the algebra map from `R` to the multivariate power series over `A` in the variable `σ` to `r` is equivalent to applying the map `MvPowerSeries.C` to the result of applying the algebra map from `R` to `A` to `r`. In simple terms, it says that the multivariate power series of an element in a given algebra structure can be computed by first mapping the element to the algebra and then constructing a constant multivariate power series from this mapped value.
More concisely: For any commutative semiring `R`, type `σ`, semiring `A` with an algebra structure over `R`, and element `r` in `R`, the application of the algebra map from `R` to the multivariate power series over `A` in the variable `σ` to `r` equals the constant multivariate power series over `A` obtained from applying the algebra map from `R` to `A` to `r`.
|
MvPowerSeries.monomial_def
theorem MvPowerSeries.monomial_def :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ),
MvPowerSeries.monomial R n = LinearMap.stdBasis R (fun x => R) n
This theorem establishes that for any type `σ`, type `R` with a semiring structure, and any function `n` from `σ` to natural numbers, the `n`-th monomial of a multivariate formal power series over `R` is equivalent to the standard basis over `R` evaluated at `n`. This is the case provided that equality between elements of `σ` is decidable. In mathematical terms, it asserts the correspondence between the `n`-th monomial in a power series and the `n`-th basis vector in a vector space over a semiring.
More concisely: For any type `σ` with decidable equality, type `R` with a semiring structure, and function `n` from `σ` to natural numbers, the `n`-th monomial of a multivariate formal power series over `R` equals the standard basis vector evaluated at `n`.
|
MvPowerSeries.coeff_monomial_same
theorem MvPowerSeries.coeff_monomial_same :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (a : R),
(MvPowerSeries.coeff R n) ((MvPowerSeries.monomial R n) a) = a
This theorem states that for any semiring `R`, any multivariate formal power series `MvPowerSeries σ R`, and any coefficient `a` of type `R`, if you apply the `n`th coefficient function `MvPowerSeries.coeff R n` to the result of applying the `n`th monomial function `MvPowerSeries.monomial R n` to `a`, you get `a` back. In other words, the `n`th coefficient of the `n`th monomial of `a` is `a` itself. This theorem essentially captures the property that the `n`th monomial maps an element of the semiring to a power series where the `n`th coefficient is that element and all other coefficients are zero.
More concisely: For any semiring `R`, `MvPowerSeries σ R a n`, where `σ` is the `n`th monomial and `a` is an element of `R` with `n`th coefficient `a`, holds that `MvPowerSeries.coeff R σ a n = a`.
|
MvPowerSeries.coeff_C_mul
theorem MvPowerSeries.coeff_C_mul :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R),
(MvPowerSeries.coeff R n) ((MvPowerSeries.C σ R) a * φ) = a * (MvPowerSeries.coeff R n) φ
The theorem `MvPowerSeries.coeff_C_mul` states that, for any semiring `R`, any index set `σ`, any multivariate formal power series `φ` over `R` indexed by `σ`, any coefficient `a` in `R`, and any `n` in the power multi-set of `σ`, the `n`-th coefficient of the product of the constant multivariate formal power series defined by `a` and `φ` is equal to `a` times the `n`-th coefficient of `φ`. This means that, in the context of multivariate formal power series, multiplication by a constant behaves as expected with respect to coefficients.
More concisely: For any semiring R, multivariate formal power series φ over R indexed by σ, coefficient a in R, and index n in the power multi-set of σ, the (n)-th coefficient of the product of the constant series a and φ is equal to a times the (n)-th coefficient of φ.
|
MvPowerSeries.map_C
theorem MvPowerSeries.map_C :
∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (a : R),
(MvPowerSeries.map σ f) ((MvPowerSeries.C σ R) a) = (MvPowerSeries.C σ S) (f a)
The theorem `MvPowerSeries.map_C` states that for any types `σ`, `R`, `S` with `R` and `S` being semirings, and for each ring homomorphism `f` from `R` to `S` and each element `a` of `R`, the operation of first applying the constant homomorphism `MvPowerSeries.C σ R` to `a` to get a multivariate power series over `R` and then applying the map `MvPowerSeries.map σ f` to the result is the same as first applying `f` to `a` to get an element of `S` and then applying the constant homomorphism `MvPowerSeries.C σ S` to the result. In other words, mapping and constant conversion commute in this context.
More concisely: For any semirings R and S, ring homomorphism f from R to S, and element a in R, the constant homomorphism applied to a in R and then mapped to S using f is equal to mapping a in R to S using f and then applying the constant homomorphism in S.
|
MvPowerSeries.coeff_mul
theorem MvPowerSeries.coeff_mul :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R) [inst_1 : DecidableEq σ],
(MvPowerSeries.coeff R n) (φ * ψ) =
(Finset.antidiagonal n).sum fun p => (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ
The theorem `MvPowerSeries.coeff_mul` is about the multiplication operation in the ring of multivariate formal power series. Given variables `σ`, a coefficient ring `R` which is a semiring, two multivariate formal power series `φ` and `ψ`, and a function `n` from `σ` to natural numbers, the theorem states that the `n`th coefficient of the product of `φ` and `ψ` is equal to the sum, over all pairs of natural number functions whose sum equals `n`, of the product of corresponding coefficients in `φ` and `ψ`. This sum is taken over the antidiagonal of `n`, which represents all pairs of natural number functions whose sum equals `n`. The equality holds under the assumption that equality of variables `σ` is decidable. In mathematical terms, this theorem formalizes how to compute the `n`th coefficient of the product of two power series in a semiring.
More concisely: Given multivariate formal power series φ and ψ over a semiring R, and variables σ with decidable equality, the (n)(i) + (n)(j) = nth coefficient of the product φψ is the sum over the antidiagonal of pairs (i, j) of the products of the i-th coefficient of φ and j-th coefficient of ψ.
|
MvPowerSeries.coeff_zero_X
theorem MvPowerSeries.coeff_zero_X :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (s : σ), (MvPowerSeries.coeff R 0) (MvPowerSeries.X s) = 0 := by
sorry
The theorem `MvPowerSeries.coeff_zero_X` states that for any type `σ` and any type `R` with a semiring structure, and for any variable `s` of type `σ`, the zero-th coefficient of the multivariate formal power series in the variable `s` is zero. In other words, if you look at the formal power series for a given variable and try to extract the coefficient of the term of degree zero, you will always get the zero element of the ring `R`.
More concisely: For any semiring `R` and variable `s` of type `σ`, the zero-th coefficient of the multivariate formal power series in `s` over `R` is the additive identity element of `R`.
|
MvPowerSeries.ext_iff
theorem MvPowerSeries.ext_iff :
∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {φ ψ : MvPowerSeries σ R},
φ = ψ ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ
This theorem states that two multivariate formal power series, denoted φ and ψ, are equal if and only if all of their coefficients are equal. These power series are defined over a coefficient ring `R` and an index set of variables `σ`. Specifically, for every `n`, which is a function mapping `σ` to non-negative integers, the `n`th coefficient of the power series φ is equal to the `n`th coefficient of the power series ψ. The equality of coefficients is checked using a semiring structure on `R`.
More concisely: Two multivariate formal power series φ and ψ over a coefficient ring R and index set σ are equal if and only if their respective coefficients of all monomials indexed by n in σ agree in R.
|