MvPolynomial.sumToIter_C
theorem MvPolynomial.sumToIter_C :
∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : R),
(MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.C a) = MvPolynomial.C (MvPolynomial.C a)
The theorem `MvPolynomial.sumToIter_C` establishes that for any commutative semiring `R` and any types `S₁` and `S₂`, and for any element `a` of `R`, when you apply `MvPolynomial.sumToIter` (a function that transforms a multivariable polynomial in a sum of two types `S₁` and `S₂`, to a multivariable polynomial in one of the types, with coefficients in multivariable polynomials in the other type) to the constant polynomial with value `a`, the result is the constant polynomial with its value being the constant polynomial of `a`. In other words, this theorem demonstrates that the `sumToIter` operation preserves the structure of constant polynomials in the input multivariable polynomial.
More concisely: For any commutative semiring R and types S₁, S₂, and element a in R, the application of `MvPolynomial.sumToIter` to the constant polynomial of value a results in the constant polynomial of value a.
|
MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le
theorem MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le :
∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ),
((MvPolynomial.finSuccEquiv R n) f).coeff i ≠ 0 →
(((MvPolynomial.finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree
This theorem states that for any commutative semiring `R`, any natural number `n`, any multivariable polynomial `f` whose variables are indexed by `Fin (n + 1)` and whose coefficients are in `R`, and any natural number `i`, if the `i`-th coefficient of the polynomial obtained by applying the algebra isomorphism `finSuccEquiv` to `f` is nonzero, then the total degree of this coefficient plus `i` is at most the total degree of `f`. In simple terms, this theorem places a bound on the degree of each coefficient of the transformed polynomial in relation to the degree of the original polynomial.
More concisely: For any commutative semiring `R`, any multivariate polynomial `f` over `R` indexed by `Fin (n + 1)`, and any `i`, the `i`-th coefficient of the polynomial `finSuccEquiv` applied to `f` has degree at most the total degree of `f` + `i`.
|
MvPolynomial.finSuccEquiv_apply
theorem MvPolynomial.finSuccEquiv_apply :
∀ (R : Type u) [inst : CommSemiring R] (n : ℕ) (p : MvPolynomial (Fin (n + 1)) R),
(MvPolynomial.finSuccEquiv R n) p =
(MvPolynomial.eval₂Hom (Polynomial.C.comp MvPolynomial.C) fun i =>
Fin.cases Polynomial.X (fun k => Polynomial.C (MvPolynomial.X k)) i)
p
The theorem `MvPolynomial.finSuccEquiv_apply` states that for any commutative semiring `R` and any natural number `n`, the application of the algebra isomorphism `finSuccEquiv`, which converts multivariable polynomials in `Fin (n + 1)` to polynomials over multivariable polynomials in `Fin n`, to any multivariable polynomial `p` in `Fin (n + 1)` is equal to the result of evaluating `p` with a specific ring homomorphism and a function.
This specific ring homomorphism is the composition of the polynomial constant `Polynomial.C` and the multivariable polynomial constant `MvPolynomial.C`. The function takes a natural number `i` and, if `i` is zero, it returns the polynomial variable `Polynomial.X`. Otherwise, for `i` equal to the successor of `k`, it returns the constant polynomial with value equal to the degree `1` monomial `MvPolynomial.X k`.
More concisely: For any commutative semiring R and natural number n, the application of `finSuccEquiv` to a multivariable polynomial p in Fin (n + 1) is equivalent to evaluating p under the homomorphism Polynomial.C ∘ MvPolynomial.C and the function that maps i to the degree 1 monomial X i if i ≠ 0, or X if i = 0.
|
MvPolynomial.finSuccEquiv_coeff_coeff
theorem MvPolynomial.finSuccEquiv_coeff_coeff :
∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ),
MvPolynomial.coeff m (((MvPolynomial.finSuccEquiv R n) f).coeff i) = MvPolynomial.coeff (Finsupp.cons i m) f
This theorem, `MvPolynomial.finSuccEquiv_coeff_coeff`, states that for any commutative semiring `R`, natural number `n`, function `m` mapping from `Fin n` to natural numbers, multivariate polynomial `f` with coefficients in `R` and variables indexed by `Fin (n + 1)`, and natural number `i`, the coefficient of `m` in the `i`-th coefficient of the polynomial obtained by applying the algebra isomorphism `finSuccEquiv R n` to `f` is equal to the coefficient of `Finsupp.cons i m` in `f`. In essence, this theorem connects the coefficients of a multivariable polynomial and its transformed polynomial under the algebra isomorphism `finSuccEquiv`.
More concisely: For any commutative semiring `R`, natural number `n`, function `m` from `Fin n` to natural numbers, multivariate polynomial `f` with coefficients in `R` and variables indexed by `Fin (n + 1)`, and natural number `i`, the coefficient of `m` in the `i`-th coefficient of the polynomial `finSuccEquiv R n` applied to `f` is equal to the coefficient of `Finsupp.cons i m` in `f`.
|