MvPolynomial.eval_add
theorem MvPolynomial.eval_add :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R},
(MvPolynomial.eval f) (p + q) = (MvPolynomial.eval f) p + (MvPolynomial.eval f) q
The theorem `MvPolynomial.eval_add` states that for any commutative semiring `R`, any type `σ`, any two multivariate polynomials `p` and `q` over `R` with variables indexed by `σ`, and any function `f` from `σ` to `R`, the evaluation of the sum of `p` and `q` using `f` is equal to the sum of the evaluations of `p` and `q` using `f`. In other words, it affirms the distributivity of polynomial evaluation over polynomial addition.
More concisely: For any commutative semiring R, type σ, multivariate polynomials p and q over R with variables indexed by σ, and function f from σ to R, the evaluation of p + q using f is equal to the sum of the evaluations of p and q using f.
|
MvPolynomial.coeff_map
theorem MvPolynomial.coeff_map :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(p : MvPolynomial σ R) (m : σ →₀ ℕ), MvPolynomial.coeff m ((MvPolynomial.map f) p) = f (MvPolynomial.coeff m p)
The theorem `MvPolynomial.coeff_map` states that for any commutative semiring `R` and `S₁`, for any index set `σ`, for any ring homomorphism `f` from `R` to `S₁`, for any multivariate polynomial `p` with coefficients in `R`, and for any monomial `m`, mapping the polynomial `p` across the ring homomorphism `f` and then taking the coefficient of the monomial `m` is the same as taking the coefficient of the monomial `m` in the original polynomial `p` and then applying the ring homomorphism `f` to it. In other words, the process of taking coefficients commutes with the process of mapping across a ring homomorphism.
More concisely: For any commutative semiring homomorphism `f` and multivariate polynomial `p` over a commutative semiring `R`, the coefficient of any monomial `m` in `p` is equal to the image under `f` of the coefficient of `m` in `p`.
|
MvPolynomial.aeval_def
theorem MvPolynomial.aeval_def :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : Algebra R S₁] (f : σ → S₁) (p : MvPolynomial σ R),
(MvPolynomial.aeval f) p = MvPolynomial.eval₂ (algebraMap R S₁) f p
The theorem `MvPolynomial.aeval_def` states that for any commutative semiring `R`, any commutative semiring `S₁` that also has an algebra structure over `R`, any type `σ`, any function `f` from `σ` to `S₁`, and any multivariate polynomial `p` with variables indexed by `σ` and coefficients in `R`, the application of the algebra homomorphism `MvPolynomial.aeval f` to `p` is equal to the evaluation `MvPolynomial.eval₂ (algebraMap R S₁) f p`. Here, `MvPolynomial.aeval f` is an algebra homomorphism generated by a map from `σ` to `S₁`, `MvPolynomial.eval₂` evaluates a polynomial `p` given a valuation `f` of all the variables and a ring homomorphism from `R` to `S₁` (in this case `algebraMap R S₁`), and `algebraMap R S₁` is the embedding from `R` to `S₁` given by the `Algebra` structure.
More concisely: For any commutative semirings R and S₁ with S₁ being an algebra over R, any type σ, any function f : σ → S₁, and any multivariate polynomial p with variables indexed by σ and coefficients in R, the application of the algebra homomorphism MvPolynomial.aeval f to p is equal to the evaluation MvPolynomial.eval₂ (algebraMap R S₁) f of p with respect to the valuation f and the ring homomorphism algebraMap R S₁.
|
MvPolynomial.eval₂Hom_congr
theorem MvPolynomial.eval₂Hom_congr :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f₁ f₂ : R →+* S₁}
{g₁ g₂ : σ → S₁} {p₁ p₂ : MvPolynomial σ R},
f₁ = f₂ → g₁ = g₂ → p₁ = p₂ → (MvPolynomial.eval₂Hom f₁ g₁) p₁ = (MvPolynomial.eval₂Hom f₂ g₂) p₂
The theorem `MvPolynomial.eval₂Hom_congr` states that for all commutative semiring, denoted as `R` and `S₁`, and a type `σ`, given two ring homomorphisms `f₁` and `f₂` from `R` to `S₁`, two functions `g₁` and `g₂` from `σ` to `S₁`, and two multivariate polynomials `p₁` and `p₂` with coefficients in `R` and variables indexed by `σ`, if `f₁` is equal to `f₂`, `g₁` is equal to `g₂`, and `p₁` is equal to `p₂`, then the result of evaluating `p₁` under the ring homomorphism `f₁` and the function `g₁` is the same as the result of evaluating `p₂` under the ring homomorphism `f₂` and the function `g₂`. This is done using the `eval₂Hom` function of `MvPolynomial`, which takes a ring homomorphism and a function as arguments and returns a ring homomorphism.
More concisely: Given commutative semirings R and S₁, ring homomorphisms f₁ = f₂ from R to S₁, functions g₁ = g₂ from a type σ to S₁, and multivariate polynomials p₁ = p₂ over R with variables indexed by σ, if f₁(x) = f₂(x) for all x in R and g₁(s) = g₂(s) for all s in σ, then MvPolynomial.eval₂Hom f₁ g₁(p₁) = MvPolynomial.eval₂Hom f₂ g₂(p₂).
|
MvPolynomial.induction_on'
theorem MvPolynomial.induction_on' :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {P : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
(∀ (u : σ →₀ ℕ) (a : R), P ((MvPolynomial.monomial u) a)) →
(∀ (p q : MvPolynomial σ R), P p → P q → P (p + q)) → P p
The theorem `MvPolynomial.induction_on'` is an analogue of the `Polynomial.induction_on'` theorem for multivariate polynomials. It states that to prove a certain property `P` holds for any multivariate polynomial `p` over a commutative semiring `R`, it suffices to prove two things. First, property `P` must hold for all monomials, i.e., for any set of exponents `u` and any coefficient `a`, `P` must hold for the monomial `MvPolynomial.monomial u a`. Second, property `P` must be preserved under addition, i.e., for any two multivariate polynomials `p` and `q`, if `P` holds for `p` and `q`, then it must also hold for `p + q`.
More concisely: To prove a property holds for any multivariate polynomial over a commutative semiring, it suffices to show that it holds for all monomials and is preserved under polynomial addition.
|
MvPolynomial.constantCoeff_X
theorem MvPolynomial.constantCoeff_X :
∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (i : σ), MvPolynomial.constantCoeff (MvPolynomial.X i) = 0
This theorem states that for any commutative semiring `R` and any type `σ`, the constant coefficient of the degree `1` monomial $X_i$ is `0`. In other words, if you retrieve the constant term (the coefficient of the 0th degree term) from the polynomial representing the `i`th variable in a multivariate polynomial over a commutative semiring, it will always be `0`.
More concisely: For any commutative semiring `R` and type `σ`, the constant term of the polynomial representing the `i`th variable in a multivariate polynomial over `R` is `0`.
|
MvPolynomial.eval₂_monomial
theorem MvPolynomial.eval₂_monomial :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
(f : R →+* S₁) (g : σ → S₁),
MvPolynomial.eval₂ f g ((MvPolynomial.monomial s) a) = f a * s.prod fun n e => g n ^ e
The theorem `MvPolynomial.eval₂_monomial` states that for any given commutative semirings `R` and `S₁`, a polynomial `a` of type `R`, and a finitely supported function `s` from a type `σ` to natural numbers, along with a ring homomorphism `f` from `R` to `S₁` and a function `g` from `σ` to `S₁`, the evaluation of the polynomial `a` with exponents given by `s` under these mappings equals the product of the mapping of `a` under `f` and the product over the support of `s`, where each term in the product is the image of an element `n` under `g`, raised to the power `e`, where `e` is the value of `s` at `n`. This theorem defines how a multivariate polynomial (represented by `MvPolynomial`) with a monomial is evaluated under a given valuation and ring homomorphism.
More concisely: For any commutative semirings R and S₁, polynomial a over R, finitely supported function s from a type σ to natural numbers, ring homomorphism f from R to S₁, and function g from σ to S₁, the evaluation of polynomial a with exponents given by s under mappings f and g equals the product of the mapping of a under f and the product over the support of s, where each term is the image of an element n under g, raised to the power of s(n).
|
MvPolynomial.monomial_eq
theorem MvPolynomial.monomial_eq :
∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
(MvPolynomial.monomial s) a = MvPolynomial.C a * s.prod fun n e => MvPolynomial.X n ^ e
The theorem `MvPolynomial.monomial_eq` states that for any commutative semiring `R`, any coefficient `a` of type `R`, and any function `s` from some type `σ` to natural numbers (representing the exponents of the monomial), the monomial with coefficient `a` and exponents given by `s` is equal to the constant polynomial with value `a` times the product of the degree `1` monomial raised to its corresponding exponent for each element in the support of `s`. In other words, it describes constructing a multivariate polynomial by multiplying the coefficient with each variable (with appropriate exponent).
More concisely: For any commutative semiring `R`, coefficient `a` of type `R`, and function `s` from some type `σ` to natural numbers, the monomial with coefficient `a` and exponents given by `s` equals the constant polynomial with value `a` times the product of degree `1` monomials, each raised to the corresponding exponent in `s`.
|
MvPolynomial.eval₂Hom_zero
theorem MvPolynomial.eval₂Hom_zero :
∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂),
MvPolynomial.eval₂Hom f 0 = f.comp MvPolynomial.constantCoeff
The theorem `MvPolynomial.eval₂Hom_zero` states that for any types `R`, `S₂`, and `σ`, with `R` and `S₂` as commutative semirings, and any ring homomorphism `f` from `R` to `S₂`, when we evaluate a multivariate polynomial with coefficients in `R` and indeterminates `σ` at zero using `MvPolynomial.eval₂Hom` with the ring homomorphism `f`, it is equivalent to first applying the constant coefficient function `MvPolynomial.constantCoeff` to the polynomial and then applying the ring homomorphism `f`. In other words, we can either evaluate the polynomial at zero and then map the result through `f`, or we can first extract the constant term of the polynomial and then map that constant term through `f`. These two processes yield the same result.
More concisely: For any commutative semirings R and S₂, ring homomorphism f from R to S₂, multivariate polynomial P with coefficients in R and indeterminates σ, we have MvPolynomial.eval₂Hom (P) (0) (f) = MvPolynomial.constantCoeff P ∘ f.
|
MvPolynomial.map_map
theorem MvPolynomial.map_map :
∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
(f : R →+* S₁) [inst_2 : CommSemiring S₂] (g : S₁ →+* S₂) (p : MvPolynomial σ R),
(MvPolynomial.map g) ((MvPolynomial.map f) p) = (MvPolynomial.map (g.comp f)) p
The theorem `MvPolynomial.map_map` states that for any multivariate polynomial `p` with coefficients in a commutative semiring `R`, and ring homomorphisms `f` from `R` to another commutative semiring `S₁`, and `g` from `S₁` to a third commutative semiring `S₂`, the result of first mapping `p` across `f` and then across `g` is the same as mapping `p` directly across the composition of `g` and `f`. That is, the operation of mapping a multivariate polynomial across a ring homomorphism preserves the composition of homomorphisms.
More concisely: For any multivariate polynomial over a commutative semiring and ring homomorphisms from two commutative semirings, the composition of their applications to the polynomial equals the application of the polynomial to the composition of the homomorphisms.
|
MvPolynomial.exists_coeff_ne_zero
theorem MvPolynomial.exists_coeff_ne_zero :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R},
p ≠ 0 → ∃ d, MvPolynomial.coeff d p ≠ 0
This theorem states that for any multivariate polynomial `p` with coefficients in a commutative semiring `R` and variables indexed by set `σ`, if the polynomial is not zero, then there exists a monomial `d` in the polynomial such that the coefficient of `d` in `p` is not zero. In other words, any non-zero multivariate polynomial must have at least one monomial with a non-zero coefficient.
More concisely: If `p` is a non-zero multivariate polynomial with coefficients in a commutative semiring `R` and variables indexed by set `σ`, then `p` has a non-zero coefficient for some monomial `d` in `p`.
|
MvPolynomial.map_injective
theorem MvPolynomial.map_injective :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
Function.Injective ⇑f → Function.Injective ⇑(MvPolynomial.map f)
The theorem `MvPolynomial.map_injective` states that for any types `R`, `S₁`, and `σ`, where `R` and `S₁` are commutative semirings, and for any ring homomorphism `f` from `R` to `S₁`, if `f` is injective (i.e., if for any `a₁` and `a₂` in `R`, `f(a₁) = f(a₂)` implies `a₁ = a₂`), then the function that maps a multivariate polynomial over `R` to a multivariate polynomial over `S₁` using `f` is also injective. In other words, the injectivity of `f` guarantees the injectivity of the mapping operation for multivariate polynomials.
More concisely: Given commutative semirings R and S₁, and a ring homomorphism f from R to S₁ that is injective, the mapping of multivariate polynomials over R to multivariate polynomials over S₁ using f is also injective.
|
MvPolynomial.eval_mul
theorem MvPolynomial.eval_mul :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R} {f : σ → R},
(MvPolynomial.eval f) (p * q) = (MvPolynomial.eval f) p * (MvPolynomial.eval f) q
This theorem, `MvPolynomial.eval_mul`, states that for any commutative semiring `R`, any type `σ`, any two multivariate polynomials `p` and `q` over `σ` with coefficients in `R`, and any evaluation function `f` from `σ` into `R`, the evaluation of the product of `p` and `q` at `f` is equal to the product of the evaluations of `p` and `q` at `f`. In other words, the polynomial evaluation function preserves multiplication. This mirrors the well-known property of function evaluations: $(p*q)(f) = p(f) * q(f)$ for multivariate polynomials $p$ and $q$ and a function evaluation $f$.
More concisely: For any commutative semiring R, type σ, multivariate polynomials p and q over σ with coefficients in R, and evaluation function f from σ into R, the product of the evaluations of p and q at f equals the evaluation of the product of p and q at f.
|
MvPolynomial.eval₂_C
theorem MvPolynomial.eval₂_C :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(g : σ → S₁) (a : R), MvPolynomial.eval₂ f g (MvPolynomial.C a) = f a
The theorem `MvPolynomial.eval₂_C` states that for any commutative semirings `R` and `S₁`, and any ring homomorphism `f` from `R` to `S₁`, function `g` mapping from `σ` to `S₁`, and any element `a` of `R`, the evaluation of the constant polynomial `MvPolynomial.C a` (which represents a polynomial with constant value `a`) using `MvPolynomial.eval₂` with the valuation `g` and the ring homomorphism `f` is equal to the application of `f` to `a`. In other words, when we evaluate a constant polynomial, we get the constant transformed by the given ring homomorphism.
More concisely: For any commutative semirings R and S₁, ring homomorphism f from R to S₁, function g from σ to S₁, and element a in R, we have MvPolynomial.eval₂ g f (MvPolynomial.C a) = f a.
|
MvPolynomial.mem_support_iff
theorem MvPolynomial.mem_support_iff :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {m : σ →₀ ℕ},
m ∈ p.support ↔ MvPolynomial.coeff m p ≠ 0
This theorem states that for any commutative semiring `R`, any type `σ`, any multivariate polynomial `p` over variables indexed by `σ` and coefficients in `R`, and any monomial `m` represented as a function from `σ` to `ℕ`, the monomial `m` is in the support set of the polynomial `p` if and only if the coefficient of the monomial `m` in the polynomial `p` is not zero.
In other words, the support set of a multivariate polynomial contains exactly those monomials that have non-zero coefficients in the polynomial.
More concisely: The support of a multivariate polynomial over a commutative semiring equals the set of monomials with non-zero coefficients in the polynomial.
|
MvPolynomial.induction_on''
theorem MvPolynomial.induction_on'' :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
(∀ (a : R), M (MvPolynomial.C a)) →
(∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R),
a ∉ f.support →
b ≠ 0 →
M f →
M ((MvPolynomial.monomial a) b) →
M
((let_fun this := (MvPolynomial.monomial a) b;
this) +
f)) →
(∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)) → M p
The theorem `MvPolynomial.induction_on''` is a principle of mathematical induction for multivariate polynomials where the index set of the variables is `σ` and the ring of coefficients is `R`, denoted `MvPolynomial σ R`. It states that for any property `M` and any polynomial `p` of type `MvPolynomial σ R`, if `M` holds for all constant polynomials, and if `M` holds for any polynomial `f` and any monomial where the monomial's exponents do not appear in `f`'s support and its coefficient is non-zero, and `M` holds for `f` and the monomial independently, then `M` holds for the sum of `f` and the monomial. Moreover, if `M` holds for a polynomial `p` and any monomial of degree 1, `M` also holds for the product of `p` and the monomial. Then we can conclude that `M` holds for the polynomial `p`.
More concisely: Given a property `M` and a multivariate polynomial `p` over index set `σ` and ring `R`, if `M` holds for all constant polynomials and monomials not in `p`'s support, and `M(p(x) * m(x)) = M(p(x)) * M(m(x))` for all monomials `m(x)`, then `M` holds for `p`.
|
MvPolynomial.algHom_ext
theorem MvPolynomial.algHom_ext :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
{f g : MvPolynomial σ R →ₐ[R] A}, (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
This theorem states that for any type `R` with a commutative semiring structure, any type `σ`, any semiring `A` that also forms an algebra over `R`, and any two algebra homomorphisms `f` and `g` from the multivariate polynomial ring `MvPolynomial σ R` to `A`, if `f` and `g` agree on all degree `1` monomials `MvPolynomial.X i` (where `i` ranges over `σ`), then `f` and `g` are the same. In other words, an algebra homomorphism from a multivariate polynomial ring is uniquely determined by its values on the degree `1` monomials.
More concisely: Given a commutative semiring `R`, a type `σ`, a semiring `A` that is an algebra over `R` for `σ`, and two algebra homomorphisms `f` and `g` from the multivariate polynomial ring `MvPolynomial σ R` to `A`, if `f(X i) = g(X i)` for all `i ∈ σ` and `X` being the indeterminate, then `f = g`.
|
MvPolynomial.aevalTower_X
theorem MvPolynomial.aevalTower_X :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
[inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (i : σ),
(MvPolynomial.aevalTower g y) (MvPolynomial.X i) = y i
The theorem `MvPolynomial.aevalTower_X` states that for all commutative semirings `R`, `S`, and `A`, with `S` being an algebra over `R` and `A`, and for any algebra homomorphism `g` from `R` to `A` over `S`, and any function `y` from `σ` to `A`, and any element `i` of `σ`, the result of applying the algebra homomorphism induced by `g` and `y` on the `MvPolynomial` degree `1` monomial `X` at `i` is equal to `y` at `i`. In simple language, it means that evaluating a degree `1` monomial at a certain point using the defined algebra homomorphism gives the same result as directly applying the function `y` at that point.
More concisely: For any commutative semirings R, S, and A, algebra g from R to A over S, function y from σ to A, and element i of σ, the evaluation of the degree 1 monomial X at i via the induced algebra homomorphism g and y is equal to y(i).
|
MvPolynomial.is_id
theorem MvPolynomial.is_id :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (f : MvPolynomial σ R →+* MvPolynomial σ R),
f.comp MvPolynomial.C = MvPolynomial.C →
(∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n) → ∀ (p : MvPolynomial σ R), f p = p
The theorem `MvPolynomial.is_id` states that for any type `R` and index set `σ`, given a commutative semiring structure on `R`, and a ring homomorphism `f` from multivariate polynomials over `σ` and `R` to themselves, if the composition of `f` and the constant polynomial function is the constant polynomial function itself, and if for every index `n` in `σ`, `f` applied to the degree `1` monomial $X_n$ is still $X_n$, then `f` is the identity function on all multivariate polynomials over `σ` and `R`. In other words, under these conditions, for any polynomial `p`, `f(p)` equals `p`.
More concisely: Given a commutative semiring `R`, a ring homomorphism `f` from multivariate polynomials over `σ` and `R` to themselves preserving constant polynomials and monomials `X_n`, then `f` is the identity function on multivariate polynomials over `σ` and `R`.
|
MvPolynomial.as_sum
theorem MvPolynomial.as_sum :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
p = p.support.sum fun v => (MvPolynomial.monomial v) (MvPolynomial.coeff v p)
This theorem states that for any multivariate polynomial `p` over a commutative semiring `R` with `σ` as the index set of the variables, `p` can be expressed as a sum over its support. The support of `p` is the set of all `σ →₀ ℕ` (maps from `σ` to non-negative integers) for which the corresponding monomial in `p` has a non-zero coefficient. For each element `v` in the support, the `v`-th monomial of `p` (given by `MvPolynomial.monomial v`) is multiplied by its corresponding coefficient in `p` (given by `MvPolynomial.coeff v p`). The sum of these products is equal to the original polynomial `p`. This essentially says that any multivariate polynomial can be represented as a sum of its non-zero monomials.
More concisely: A multivariate polynomial over a commutative semiring can be expressed as the sum of its monomials with non-zero coefficients.
|
MvPolynomial.map_leftInverse
theorem MvPolynomial.map_leftInverse :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
{g : S₁ →+* R}, Function.LeftInverse ⇑f ⇑g → Function.LeftInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
The theorem `MvPolynomial.map_leftInverse` states that for any given types `R`, `S₁`, and `σ`, along with their respective commutative semirings, if function `f` is a left-inverse of function `g` (i.e., composing `g` after `f` gives the identity function), then the function `map f` is a left-inverse for the function `map g` in the context of multivariate polynomials. In other words, if applying `f` and then `g` to any element yields that element again (`g(f(x)) = x` for all `x`), then the same holds true for their respective `map` functions applied to any multivariate polynomial (`map g(map f(p)) = p` for all `p`).
More concisely: If `f` is a left-inverse of `g` in the context of commutative semirings, then `map f` is a left-inverse of `map g` for multivariate polynomials.
|
MvPolynomial.ringHom_ext'
theorem MvPolynomial.ringHom_ext' :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
{f g : MvPolynomial σ R →+* A},
f.comp MvPolynomial.C = g.comp MvPolynomial.C →
(∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
This theorem, denoted as `MvPolynomial.ringHom_ext'`, states that for any commutative semiring `R` with an index set of variables `σ`, and for any semiring `A`, if we have two ring homomorphisms `f` and `g` from multivariate polynomials over `R` and `σ` to `A`, and if these two homomorphisms agree on the constant polynomial and on the degree `1` monomials, then these two ring homomorphisms are indeed the same. In other words, a ring homomorphism from the ring of multivariate polynomials to another ring is uniquely determined by its values on the constant polynomials and on the degree `1` monomials.
More concisely: Given commutative semirings R with index set σ, and semiring A, if two ring homomorphisms from the multivariate polynomial ring R[σ] to A agree on the constant polynomial and degree 1 monomials, then they are equal.
|
MvPolynomial.coeff_C_mul
theorem MvPolynomial.coeff_C_mul :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (a : R) (p : MvPolynomial σ R),
MvPolynomial.coeff m (MvPolynomial.C a * p) = a * MvPolynomial.coeff m p
The theorem `MvPolynomial.coeff_C_mul` states that for any type `R` and `σ`, if `R` is a commutative semiring, then for every multi-variable polynomial `p` of type `MvPolynomial σ R`, any coefficient `a` of type `R`, and any monomial `m` of type `σ →₀ ℕ`, the coefficient of the monomial `m` in the polynomial resulting from multiplying `p` by the constant polynomial with value `a` (`MvPolynomial.C a * p`) is equal to `a` times the coefficient of the monomial `m` in `p` itself. In other words, multiplying a multivariate polynomial by a constant scales the coefficients of all monomials by that constant.
More concisely: For any commutative semiring `R` and multi-variable polynomial `p` of type `MvPolynomial σ R`, the coefficient of any monomial `m` in the product of `p` and the constant polynomial `C a` is equal to `a` times the coefficient of `m` in `p`.
|
MvPolynomial.map_id
theorem MvPolynomial.map_id :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
(MvPolynomial.map (RingHom.id R)) p = p
The theorem `MvPolynomial.map_id` states that for any commutative semiring `R` and any type `σ` (which serves as the index set of the variables), and any multivariate polynomial `p` over `R` with variables indexed by `σ`, the map of `p` across the identity ring homomorphism from `R` to itself results in the original polynomial `p` itself. In other words, applying the identity transformation to each coefficient of the multivariate polynomial does not change the polynomial.
More concisely: For any commutative semiring R and multivariate polynomial p over R indexed by type σ, the application of the identity ring homomorphism from R to itself to the coefficients of p leaves p unchanged.
|
MvPolynomial.coeff_sum
theorem MvPolynomial.coeff_sum :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {X : Type u_2} (s : Finset X) (f : X → MvPolynomial σ R)
(m : σ →₀ ℕ), MvPolynomial.coeff m (s.sum fun x => f x) = s.sum fun x => MvPolynomial.coeff m (f x)
This theorem is about the coefficients of multivariate polynomials. It states that for any commutative semiring `R`, any type `σ` and `X`, any finite set `s` of type `X`, any function `f` from `X` to multivariate polynomials over `R` with variables indexed by `σ`, and any monomial `m`, the coefficient of the monomial `m` in the polynomial that is the sum (over the set `s`) of the polynomials `f(x)` is equal to the sum (over the set `s`) of the coefficients of the monomial `m` in the polynomials `f(x)`. In mathematical terms, this is saying that the coefficient of a particular term in a sum of polynomials is just the sum of the coefficients of that term in each of the polynomials.
More concisely: For any commutative semiring `R`, given a finite set `s`, a type `X`, a function `f` from `X` to multivariate polynomials over `R` with variables indexed by `σ`, and a monomial `m`, the sum of the coefficients of `m` in the polynomials `f(x)` for all `x` in `s` equals the coefficient of `m` in the sum of the polynomials `f(x)` over `s`.
|
MvPolynomial.ringHom_ext
theorem MvPolynomial.ringHom_ext :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A]
{f g : MvPolynomial σ R →+* A},
(∀ (r : R), f (MvPolynomial.C r) = g (MvPolynomial.C r)) →
(∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
The theorem `MvPolynomial.ringHom_ext` states that for any type `R` with a commutative semiring structure, any type `σ`, any type `A` with a semiring structure, and any two ring homomorphisms `f` and `g` from the multivariate polynomials over `R` and `σ` to `A`, if `f` and `g` coincide on the constant polynomials and on the degree `1` monomials, then `f` and `g` are identical. In other words, a ring homomorphism from a multivariate polynomial ring is uniquely determined by its values on the constants and on the degree `1` monomials.
More concisely: Given commutative semirings R, type σ, semiring A, and ring homomorphisms f and g from the multivariate polynomials over R and σ to A, if f and g agree on constants and degree 1 monomials, then f = g.
|
MvPolynomial.aeval_X
theorem MvPolynomial.aeval_X :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : Algebra R S₁] (f : σ → S₁) (s : σ), (MvPolynomial.aeval f) (MvPolynomial.X s) = f s
The theorem `MvPolynomial.aeval_X` states that for any commutative semirings `R` and `S₁`, where `S₁` is an algebra over `R`, any map `f` from a type `σ` to `S₁`, and any element `s` of type `σ`, applying the algebraic evaluation map induced by `f` to the degree `1` multivariate polynomial `MvPolynomial.X s` (which corresponds to the monomial $X_s$) yields the value `f s`. In other terms, it means that the evaluation of the variable $X_s$ under the map `f` is exactly `f s`.
More concisely: For any commutative semirings R and an algebra S₁ over R, map f from type σ to S₁, and element s of type σ, the algebraic evaluation of the degree 1 multivariate polynomial MvPolynomial.X s along f equals f(s).
|
MvPolynomial.eval_X
theorem MvPolynomial.eval_X :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : σ → R} (n : σ),
(MvPolynomial.eval f) (MvPolynomial.X n) = f n
This theorem states that for any commutative semiring `R`, for any type `σ`, and for any function `f` from `σ` to `R`, if you evaluate the degree `1` monomial (indicated by `MvPolynomial.X n`) under the evaluation map `MvPolynomial.eval f`, it is equivalent to simply applying the function `f` to `n`. In other words, the evaluation of a monomial at a specific point is just the value of that point under the function `f`.
More concisely: For any commutative semiring `R`, any type `σ`, and any function `f` from `σ` to `R`, the evaluation of the degree `1` monomial `MvPolynomial.X n` under `MvPolynomial.eval f` equals `f n`.
|
MvPolynomial.map_rightInverse
theorem MvPolynomial.map_rightInverse :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {f : R →+* S₁}
{g : S₁ →+* R}, Function.RightInverse ⇑f ⇑g → Function.RightInverse ⇑(MvPolynomial.map f) ⇑(MvPolynomial.map g)
The theorem `MvPolynomial.map_rightInverse` states that for any two types `R` and `S₁` (representing rings) and a type `σ`, if the commutative semiring structures are defined on `R` and `S₁`, and `f` is a right-inverse of `g` where `f` and `g` are ring homomorphisms between `R` and `S₁` (i.e., `f ∘ g = id`), then the operation `map f` is a right-inverse of `map g` on multivariate polynomials over `R` and `S₁` respectively (i.e., `(MvPolynomial.map f) ∘ (MvPolynomial.map g) = id`). In other words, if `f` undoes the operation of `g` in the context of the rings `R` and `S₁`, then the same relationship holds for the corresponding operations on their multivariate polynomials.
More concisely: If homomorphisms `f : R → S₁` and `g : S₁ → R` satisfy `f ∘ g = id_R` and `g ∘ f = id_S₁`, then `MvPolynomial.map f` is a right-inverse of `MvPolynomial.map g` on multivariate polynomials over `R` and `S₁`.
|
Algebra.adjoin_range_eq_range_aeval
theorem Algebra.adjoin_range_eq_range_aeval :
∀ (R : Type u) {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : Algebra R S₁] (f : σ → S₁), Algebra.adjoin R (Set.range f) = (MvPolynomial.aeval f).range
This theorem states that for all commutative semirings `R` and `S₁`, and a function `f` from an arbitrary type `σ` to `S₁`, the minimal subalgebra of `S₁` that includes the range of `f` (i.e., `Algebra.adjoin R (Set.range f)`) is equal to the range of the algebra homomorphism obtained by evaluating a multivariate polynomial at `f` (i.e., `AlgHom.range (MvPolynomial.aeval f)`). In simpler terms, it says that the smallest subalgebra containing the image of `f` under `R` is the same as the image of the multivariate polynomial evaluation mapping.
More concisely: The smallest subalgebra of a commutative semiring `S₁` that includes the range of a function `f` from an arbitrary type to `S₁` is equal to the range of the multivariate polynomial evaluation homomorphism `MvPolynomial.aeval f` on `R`.
|
MvPolynomial.ext
theorem MvPolynomial.ext :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p q : MvPolynomial σ R),
(∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q) → p = q
This theorem states that for any commutative semiring `R` and any type `σ`, if we have two multivariate polynomials `p` and `q` over the variables indexed by `σ` and with coefficients in `R`, then `p` and `q` are equal if and only if their coefficients for each monomial `m` (represented as a function from `σ` to natural numbers) are equal. In other words, two multivariate polynomials are considered identical if they have the same coefficients for the same monomials.
More concisely: For any commutative semiring R and type σ, two multivariate polynomials over R with variables indexed by σ are equal if and only if their corresponding coefficient functions agree on all monomials.
|
MvPolynomial.eval_C
theorem MvPolynomial.eval_C :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {f : σ → R} (a : R),
(MvPolynomial.eval f) (MvPolynomial.C a) = a
The theorem `MvPolynomial.eval_C` states that for any type `R` representing a commutative semiring, a type `σ`, a function `f` from `σ` to `R`, and an element `a` of `R`, the evaluation of the constant multivariate polynomial with value `a` under the function `f` is equal to `a`. This means that the evaluation function applied to a constant polynomial simply returns the constant value itself, without any consideration of the function `f` or the variables in the polynomial.
More concisely: For any commutative semiring R, constant multivariate polynomial p over R, and function f : σ -> R, the evaluation of p under f is equal to the constant value p.
|
MvPolynomial.eval₂Hom_C
theorem MvPolynomial.eval₂Hom_C :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(g : σ → S₁) (r : R), (MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r
The theorem `MvPolynomial.eval₂Hom_C` states that for any types `R`, `S₁`, and `σ`, and for any commutative semirings `R` and `S₁`, given a ring homomorphism `f: R →+* S₁`, a function `g: σ → S₁`, and an element `r` of `R`, the evaluation of the constant polynomial `MvPolynomial.C r` under the homomorphism `MvPolynomial.eval₂Hom f g` is equal to the evaluation of `r` under `f`. In other words, the homomorphism `MvPolynomial.eval₂Hom f g` preserves the evaluation of constant polynomials.
More concisely: For any commutative semirings R and S₁, ring homomorphism f : R →+* S₁, function g : σ → S₁, and element r in R, we have MvPolynomial.eval₂Hom f g (MvPolynomial.C r) = f r.
|
MvPolynomial.C_1
theorem MvPolynomial.C_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.C 1 = 1
The theorem `MvPolynomial.C_1` states that for any commutative semiring `R` and any type `σ`, the constant polynomial with value `1` in the multivariate polynomial ring over `R` in variables from `σ` is equal to `1`. In other words, when we consider the constant polynomial that takes the value `1`, it acts as the multiplicative identity in the ring of multivariate polynomials, just as `1` does in the base ring `R`.
More concisely: For any commutative semiring R and type σ, the constant polynomial in the multivariate polynomial ring over R with variables from σ equals the multiplicative identity.
|
MvPolynomial.X_pow_eq_monomial
theorem MvPolynomial.X_pow_eq_monomial :
∀ {R : Type u} {σ : Type u_1} {e : ℕ} {n : σ} [inst : CommSemiring R],
MvPolynomial.X n ^ e = (MvPolynomial.monomial fun₀ | n => e) 1
This theorem states that for any commutative semiring `R`, any type `σ`, any natural number `e`, and any element `n` of type `σ`, the `e`th power of the `n`th degree 1 monomial is equal to the monomial with coefficient `1` and exponents given by the function that maps `n` to `e` and all other elements of `σ` to `0`. In other words, taking the `e`th power of the `n`th degree 1 monomial in a multivariable polynomial over a commutative semiring results in a monomial whose exponent for `n` is `e` and whose coefficient is `1`.
More concisely: For any commutative semiring `R` and any `σ`, the `e`th power of the monomial `x^n` in `R[σ]` equals `x^(map n e)`, where `n : σ → ℕ`, `e : ℕ`, and `map` is function application.
|
MvPolynomial.map_C
theorem MvPolynomial.map_C :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(a : R), (MvPolynomial.map f) (MvPolynomial.C a) = MvPolynomial.C (f a)
The `MvPolynomial.map_C` theorem states that for any commutative semirings `R` and `S₁`, and any ring homomorphism `f` from `R` to `S₁`, the operation of mapping a constant polynomial `C a` from `R` to `S₁` using `f` is the same as creating a new constant polynomial in `S₁` with the value `f a`. In other words, applying the map to the constant polynomial is equivalent to applying the homomorphism to the constant value and then creating a constant polynomial with the result.
More concisely: For any commutative semirings R and S₁, and ring homomorphism f from R to S₁, the map of a constant polynomial C a from R to S₁ using f is equivalent to the constant polynomial in S₁ with value f(a).
|
MvPolynomial.coeff_add
theorem MvPolynomial.coeff_add :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (p q : MvPolynomial σ R),
MvPolynomial.coeff m (p + q) = MvPolynomial.coeff m p + MvPolynomial.coeff m q
This theorem states that for any commutative semiring `R`, any index set `σ`, any monomial `m` (which is a function from `σ` to ℕ), and any two multivariate polynomials `p` and `q` (where the polynomials' coefficients are from `R` and their variables are indexed by `σ`), the coefficient of `m` in the polynomial resulting from the addition of `p` and `q` is equal to the sum of the coefficients of `m` in `p` and `q`. This property is analogous to the distributive law in algebra, but applied to the coefficients of multivariate polynomials.
More concisely: For any commutative semiring `R`, any index set `σ`, and multivariate polynomials `p` and `q` over `R` with coefficients indexed by `σ`, the coefficient of any monomial `m` in the sum of `p` and `q` is the sum of the coefficients of `m` in `p` and `q`.
|
MvPolynomial.aeval_C
theorem MvPolynomial.aeval_C :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : Algebra R S₁] (f : σ → S₁) (r : R), (MvPolynomial.aeval f) (MvPolynomial.C r) = (algebraMap R S₁) r
The theorem `MvPolynomial.aeval_C` states that for any types `R`, `S₁`, `σ` where `R` is a commutative semiring, `S₁` is a commutative semiring and an algebra over `R`, and `f` is a map from `σ` to `S₁`, and for any element `r` of `R`, applying the algebra homomorphism generated by `f` to the constant polynomial with value `r` is equivalent to applying the algebra embedding from `R` to `S₁` to `r`. In other words, evaluating the constant polynomial using a certain algebra homomorphism returns the same result as mapping the constant value via the algebra embedding.
More concisely: For any commutative semirings R and S₁, algebra homomorphism f : σ -> S₁, and r ∈ R, we have f.(constant polynomial of value r) = algebra embedding of R into S₁ (r).
|
MvPolynomial.coeff_monomial
theorem MvPolynomial.coeff_monomial :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m n : σ →₀ ℕ) (a : R),
MvPolynomial.coeff m ((MvPolynomial.monomial n) a) = if n = m then a else 0
The theorem `MvPolynomial.coeff_monomial` states that for any commutative semiring `R`, types `σ` and `R`, and for any pair of natural number-valued functions `m` and `n` on `σ`, and any element `a` of `R`, the coefficient of the monomial `m` in the multi-variable polynomial obtained by applying the `MvPolynomial.monomial` function to `n` and `a`, is `a` if `n` equals `m`, and `0` otherwise. This theorem essentially captures how the coefficient function interacts with the construction of a monomial: if the monomial we're considering is the one we used to construct the polynomial, its coefficient is just the coefficient we used in the construction; if not, the coefficient is zero.
More concisely: For any commutative semiring R, function m : σ -> Nat, and elements a in R and n in σ, the coefficient of the monomial MvPolynomial.monomial n in the polynomial obtained by applying MvPolynomial.coeff_monomial a m, is a if n equals m, and 0 otherwise.
|
MvPolynomial.eval₂Hom_map_hom
theorem MvPolynomial.eval₂Hom_map_hom :
∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R),
(MvPolynomial.eval₂Hom φ g) ((MvPolynomial.map f) p) = (MvPolynomial.eval₂Hom (φ.comp f) g) p
This theorem states that for all types `R`, `S₁`, `S₂`, and `σ`, commutative semirings `R`, `S₁`, and `S₂`, a ring homomorphism `f` from `R` to `S₁`, a function `g` from `σ` to `S₂`, a ring homomorphism `φ` from `S₁` to `S₂`, and a multivariate polynomial `p` over `σ` and `R`, the evaluation of the polynomial `p` mapped via `f` with `φ` and `g` is equivalent to the evaluation of the polynomial `p` with the composition of `φ` and `f`, and `g`. Essentially, this theorem presents the commutativity of the processes of mapping and evaluation of multivariate polynomials.
More concisely: For commutative semirings R, S₁, S₂, ring homomorphisms f : R → S₁, φ : S₁ → S₂, function g : σ → S₂, and multivariate polynomial p over σ and R, we have that f(p(x₁, ..., xn)) = φ(p(fx₁, ..., fxn)) + g, where the addition is in S₂.
|
MvPolynomial.coeff_zero
theorem MvPolynomial.coeff_zero :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ), MvPolynomial.coeff m 0 = 0
The theorem `MvPolynomial.coeff_zero` states that for any type `R` with a commutative semiring structure and any type `σ`, the coefficient of the monomial `m` (represented as a function from `σ` to `ℕ`) in the zero multi-variable polynomial over `R` is always zero. This is a standard property of polynomials: the zero polynomial has all coefficients equal to zero.
More concisely: For any commutative semiring `R` and any monomial `m` of a multi-variable polynomial over `R`, the coefficient of `m` in the zero polynomial is zero.
|
MvPolynomial.C_mul_monomial
theorem MvPolynomial.C_mul_monomial :
∀ {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
MvPolynomial.C a * (MvPolynomial.monomial s) a' = (MvPolynomial.monomial s) (a * a')
The theorem `MvPolynomial.C_mul_monomial` states that for any type `R` forming a commutative semi-ring, any type `σ`, any `R` values `a` and `a'`, and any function `s` mapping `σ` to natural numbers, the constant polynomial with value `a` multiplied by the monomial with coefficient `a'` and exponents given by `s` is equal to the monomial with the coefficient `a * a'` and exponents given by `s`. This theorem essentially captures the distributive property of multiplication over constant and monomial polynomials in the context of multivariate polynomials.
More concisely: For any commutative semi-ring type R, any type σ, and functions s from σ to natural numbers, the constant polynomial `a` multiplied by the monomial `a' × x^(s)` is equal to the monomial `(a × a') × x^(s)`, where x represents a variable of type σ.
|
MvPolynomial.aevalTower_C
theorem MvPolynomial.aevalTower_C :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
[inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R),
(MvPolynomial.aevalTower g y) (MvPolynomial.C x) = g x
The theorem `MvPolynomial.aevalTower_C` states that for any types `R`, `σ`, `S`, and `A` with `R`, `S`, and `A` being commutative semirings and `S` being an algebra over `R` and `A`, and given an algebra homomorphism `g` from `R` to `A` over `S`, a function `y` from `σ` to `A`, and an element `x` of `R`, the result of applying the `MvPolynomial.aevalTower` function to `g` and `y` and then applying the result to the constant polynomial `MvPolynomial.C x` is equal to `g x`. This theorem essentially links the algebra homomorphism `g` and the function `MvPolynomial.aevalTower`, when evaluated at a constant polynomial, resulting in the same value as directly applying `g` to `x`.
More concisely: For any commutative semirings R, S, and A, an algebra S over R and A, an algebra homomorphism g from R to A over S, a function y from σ to A, and an element x of R, the application of `MvPolynomial.aevalTower` to g, y, and `MvPolynomial.C x` equals g(x).
|
MvPolynomial.eval₂Hom_zero_apply
theorem MvPolynomial.eval₂Hom_zero_apply :
∀ {R : Type u} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₂] (f : R →+* S₂)
(p : MvPolynomial σ R), (MvPolynomial.eval₂Hom f 0) p = f (MvPolynomial.constantCoeff p)
This theorem states that for any commutative semiring `R` and `S₂`, and for any index set `σ`, if `f` is a ring homomorphism from `R` to `S₂` and `p` is a multivariate polynomial with variables indexed by `σ` and coefficients in `R`, then evaluating `p` at `0` using `eval₂Hom` with `f` and `0` as arguments is equal to applying `f` to the constant coefficient of `p`. In other words, the theorem describes a property of the evaluation of a polynomial at zero.
More concisely: For any commutative semiring `R`, index set `σ`, ring homomorphism `f` from `R` to `S₂`, and multivariate polynomial `p` with coefficients in `R` indexed by `σ`, we have `eval₂Hom f 0 p = f (const_num p)`, where `const_num p` denotes the constant coefficient of `p`.
|
MvPolynomial.eval₂Hom_X'
theorem MvPolynomial.eval₂Hom_X' :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(g : σ → S₁) (i : σ), (MvPolynomial.eval₂Hom f g) (MvPolynomial.X i) = g i
The theorem `MvPolynomial.eval₂Hom_X'` states that for any types `R`, `S₁`, and `σ`, given two commutative semirings `R` and `S₁`, a ring homomorphism `f` from `R` to `S₁`, a function `g` from `σ` to `S₁`, and a value `i` of type `σ`, the application of the ring homomorphism `MvPolynomial.eval₂Hom f g` to the multivariable polynomial `MvPolynomial.X i` (which represents a degree `1` monomial) is equivalent to applying the function `g` to `i`. In mathematical terms, this theorem asserts that for a given ring homomorphism and a function, the evaluation of the degree `1` monomial at a certain variable using the `eval₂Hom` function is the same as the function's value at that variable.
More concisely: For any commutative semirings R and S₁, ring homomorphism f : R → S₁, function g : σ → S₁, and value i : σ, the application of MvPolynomial.eval₂Hom f g to the multivariable polynomial MvPolynomial.X i equals g i.
|
MvPolynomial.C_0
theorem MvPolynomial.C_0 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], MvPolynomial.C 0 = 0
The theorem `MvPolynomial.C_0` states that for any commutative semiring `R` and any type `σ`, the constant multivariate polynomial with value `0` (i.e., `MvPolynomial.C 0`) is equal to the zero polynomial. This is a general result that holds for any choice of `R` and `σ`, which might represent, for example, the coefficients and variables of the polynomial respectively.
More concisely: For any commutative semiring `R` and type `σ`, the constant multivariate polynomial `MvPolynomial.C 0` equals the zero polynomial.
|
MvPolynomial.support_monomial
theorem MvPolynomial.support_monomial :
∀ {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ ℕ} [inst : CommSemiring R] [h : Decidable (a = 0)],
((MvPolynomial.monomial s) a).support = if a = 0 then ∅ else {s}
This theorem states that for any type `R`, any type `σ`, any element `a` of type `R`, and any function `s` from `σ` to natural numbers `ℕ` in a commutative semiring `R`, if we can decide whether `a` is zero or not, then the support of the multivariate polynomial monomial `a` with exponents given by `s` is either an empty set if `a` is zero, or a set containing just `s` if `a` isn't zero. The support of a multivariate polynomial is the finite set of all `m : σ →₀ ℕ` such that `X^m` has a non-zero coefficient.
More concisely: For any commutative semiring R, type σ, element a of R, and function s from σ to natural numbers, if a is zero then the support of the multivariate polynomial monomial a with exponents given by s is empty, otherwise it is a singleton set containing s.
|
MvPolynomial.C_injective
theorem MvPolynomial.C_injective :
∀ (σ : Type u_2) (R : Type u_3) [inst : CommSemiring R], Function.Injective ⇑MvPolynomial.C
The theorem `MvPolynomial.C_injective` states that for any type `σ` and any type `R` (where `R` is a commutative semiring), the function `MvPolynomial.C`, which generates a constant polynomial with value from `R`, is injective. This means that if two constant polynomials are equal, then their corresponding values from `R` are also equal. In other words, no two different values from the commutative semiring `R` can yield the same constant polynomial when passed through the `MvPolynomial.C` function.
More concisely: The function `MvPolynomial.C` mapping elements of a commutative semiring `R` to the constant polynomials over a type `σ` is an injection.
|
MvPolynomial.induction_on
theorem MvPolynomial.induction_on :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
(∀ (a : R), M (MvPolynomial.C a)) →
(∀ (p q : MvPolynomial σ R), M p → M q → M (p + q)) →
(∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * MvPolynomial.X n)) → M p
This theorem is a form of mathematical induction for multivariate polynomials. Specifically, it states that for any kind of commutative semiring `R` and any type `σ`, if we have a property `M` that holds for all constant polynomials, is preserved under addition of any two multivariate polynomials `p` and `q` where `M` holds for both `p` and `q`, and is preserved under multiplication of any multivariate polynomial `p` by a monomial `MvPolynomial.X n` where `M` holds for `p`, then `M` holds for all multivariate polynomials `p` of type `MvPolynomial σ R`.
More concisely: If `M` is a property that holds for all constant multivariate polynomials `R[x₁, …, xₙ]`, is closed under addition and multiplication, then `M` holds for all multivariate polynomials `p` of type `R[x₁, …, xₙ]`.
|
MvPolynomial.C_mul'
theorem MvPolynomial.C_mul' :
∀ {R : Type u} {σ : Type u_1} {a : R} [inst : CommSemiring R] {p : MvPolynomial σ R},
MvPolynomial.C a * p = a • p
This theorem states that for any commutative semiring `R`, any type `σ`, any element `a` of `R`, and any multivariate polynomial `p` with variables indexed by `σ` and coefficients in `R`, the result of multiplying the constant polynomial with value `a` by `p` (using the function `MvPolynomial.C a * p`) is the same as scaling `p` by `a` (using the scalar multiplication `a • p`). In other words, in this context, polynomial multiplication with a constant behaves like scalar multiplication.
More concisely: For any commutative semiring `R`, any type `σ`, any element `a` of `R`, and any multivariate polynomial `p` over `R` indexed by `σ`, the constant polynomial `a` multiplied with `p` is equivalent to scaling `p` by `a`.
|
MvPolynomial.coeff_mul
theorem MvPolynomial.coeff_mul :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R)
(n : σ →₀ ℕ),
MvPolynomial.coeff n (p * q) =
(Finset.antidiagonal n).sum fun x => MvPolynomial.coeff x.1 p * MvPolynomial.coeff x.2 q
This theorem, `MvPolynomial.coeff_mul`, states that for any commutative semiring `R` and any type `σ` with decidable equality, given two multi-variable polynomials `p` and `q` over `R` and `σ`, and any monomial `n`, the coefficient of the monomial `n` in the product of polynomials `p` and `q` is equal to the sum, over all pairs of monomials `(x.1, x.2)` such that they add up to `n`, of the product of the coefficient of `x.1` in `p` and the coefficient of `x.2` in `q`. In mathematical notation, this can be written as $(p*q)_n = \sum_{(i,j) \in S} p_i * q_j$, where $S = \{(i,j) | i+j=n\}$ and $(p*q)_n$ denotes the coefficient of monomial `n` in the product of `p` and `q`.
More concisely: The coefficient of a monomial in the product of two multi-variable polynomials is the sum of the products of the coefficients of corresponding monomials in the factors, for all monomials that sum up to the target monomial.
|
MvPolynomial.coeff_C
theorem MvPolynomial.coeff_C :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ) (a : R),
MvPolynomial.coeff m (MvPolynomial.C a) = if 0 = m then a else 0
The theorem `MvPolynomial.coeff_C` states that for any commutative semiring `R`, any type `σ` with decidable equality, any multivariate monomial `m` in `σ`, and any element `a` of `R`, the coefficient of the monomial `m` in the constant multivariate polynomial `C a` is `a` if `m` is zero, and `0` otherwise. In other words, the constant multivariate polynomial `C a` has coefficient `a` for the zero monomial and coefficient `0` for all other monomials.
More concisely: For any commutative semiring R, multivariate monomial m, and element a in R, the constant multivariate polynomial C a has coefficient a for the zero monomial m and coefficient 0 for all other monomials.
|
MvPolynomial.constantCoeff_C
theorem MvPolynomial.constantCoeff_C :
∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] (r : R), MvPolynomial.constantCoeff (MvPolynomial.C r) = r
The theorem `MvPolynomial.constantCoeff_C` states that for any type `R` with a commutative semiring structure and any type `σ`, and for any element `r` of type `R`, the constant coefficient of the constant polynomial with value `r` is `r` itself. In other words, when we create a constant polynomial with some value `r`, the constant term of that polynomial is precisely `r`. This holds in any commutative semiring.
More concisely: For any commutative semiring (R, +, \*), and any element r in R, the constant polynomial over R with constant term r equals r itself.
|
MvPolynomial.map_aeval
theorem MvPolynomial.map_aeval :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
[inst_2 : Algebra R S₁] {B : Type u_2} [inst_3 : CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B)
(p : MvPolynomial σ R),
φ ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p
The theorem `MvPolynomial.map_aeval` states that for any commutative semirings `R`, `S₁`, and `B`, any algebra structure from `R` to `S₁`, a function `g` from an arbitrary type `σ` to `S₁`, a ring homomorphism `φ` from `S₁` to `B`, and a multivariate polynomial `p` over `σ` and `R`, the image of the polynomial `p` under the `R`-algebra homomorphism generated by `g` (denoted as `(MvPolynomial.aeval g) p`), when further mapped through `φ`, is the same as the image of `p` under the ring homomorphism generated by composing `φ` with the embedding of `R` into `S₁`, and mapping each variable indexed by `σ` through `φ` after `g`. In mathematical notation, this is saying that for all such settings, we have `φ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ (algebraMap R S₁)) (λ i, φ(g i)) p`.
More concisely: For any commutative semirings R, S₁, and B, an algebra homomorphism from R to S₁, a ring homomorphism from S₁ to B, a multivariate polynomial p over R and a type σ, we have φ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (RingHom.comp φ (algebraMap R S₁)) (λ i, φ(gi)) p).
|
MvPolynomial.ext_iff
theorem MvPolynomial.ext_iff :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p q : MvPolynomial σ R),
p = q ↔ ∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q
This theorem states that for any commutative semiring `R` and any type `σ`, two multivariate polynomials `p` and `q` with variables indexed by `σ` and coefficients from `R` are equal if and only if their coefficients for every monomial `m` (represented as a function from `σ` to ℕ) are equal. In other words, two multivariate polynomials are identical if they have the same coefficients for all their monomials.
More concisely: Given a commutative semiring `R` and multivariate polynomials `p` and `q` over `R` with variables indexed by `σ`, `p` equals `q` if and only if for all functions `m` from `σ` to ℕ, the coefficients of `p` and `q` corresponding to monomial `m` are equal.
|
MvPolynomial.eval_pow
theorem MvPolynomial.eval_pow :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {f : σ → R} (n : ℕ),
(MvPolynomial.eval f) (p ^ n) = (MvPolynomial.eval f) p ^ n
This theorem states that for any commutative semiring `R`, any multivariate polynomial `p` over the set of variables `σ` and the ring `R`, any function `f` that maps each variable in `σ` to a value in `R`, and any natural number `n`, evaluating the polynomial `p` raised to the power `n` (with respect to the valuation `f`) is the same as evaluating the polynomial `p` (with respect to the valuation `f`) and then raising the result to the power `n`. In other words, the evaluation function `MvPolynomial.eval` commutes with the power operation.
More concisely: For any commutative semiring `R`, any multivariate polynomial `p` over `R` and variables `σ`, and any function `f: σ -> R`, the evaluation of `p` at `f` raised to the power `n` equals the power of the evaluation of `p` at `f` by `n`.
|
MvPolynomial.induction_on'''
theorem MvPolynomial.induction_on''' :
∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {M : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
(∀ (a : R), M (MvPolynomial.C a)) →
(∀ (a : σ →₀ ℕ) (b : R) (f : (σ →₀ ℕ) →₀ R),
a ∉ f.support →
b ≠ 0 →
M f →
M
((let_fun this := (MvPolynomial.monomial a) b;
this) +
f)) →
M p
This theorem, `MvPolynomial.induction_on'''`, is a method of induction on multivariate polynomials where only a weak form of addition is required. For any multivariate polynomial `p` over a commutative semiring `R` and indexed by set `σ`, if a property `M` holds for all constant polynomials, and if for any monomial defined by a set `a` of natural number exponents, a coefficient `b` not equal to zero, and a polynomial `f` such that `a` is not in the support of `f`, if `M` holds for `f`, then `M` also holds for the polynomial defined by adding the monomial to `f`, then the property `M` must hold for `p`.
More concisely: If `M` is a property holding for all constant multivariate polynomials over a commutative semiring `R` indexed by set `σ`, and if `M` is preserved under monomial addition when a monomial does not already appear in the polynomial, then `M` holds for any multivariate polynomial `p`.
|
MvPolynomial.eval₂_add
theorem MvPolynomial.eval₂_add :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
{p q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁),
MvPolynomial.eval₂ f g (p + q) = MvPolynomial.eval₂ f g p + MvPolynomial.eval₂ f g q
The theorem `MvPolynomial.eval₂_add` asserts that for any commutative semirings `R` and `S₁`, any multivariate polynomial `p` and `q` over `R` with variables indexed by `σ`, any ring homomorphism `f` from `R` to `S₁`, and any valuation `g` of the variables, the evaluation of the sum of `p` and `q` using `f` and `g` is equal to the sum of the evaluations of `p` and `q` individually using `f` and `g`. This is the property of linearity for the evaluation of multivariate polynomials.
More concisely: For any commutative semirings R and S₁, multivariate polynomials p and q over R, ring homomorphism f from R to S₁, and valuation g, the evaluation of p + q using f and g equals the sum of the evaluations of p and q using f and g.
|
MvPolynomial.map_monomial
theorem MvPolynomial.map_monomial :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(s : σ →₀ ℕ) (a : R), (MvPolynomial.map f) ((MvPolynomial.monomial s) a) = (MvPolynomial.monomial s) (f a)
The theorem `MvPolynomial.map_monomial` states that for any commutative semirings `R` and `S₁`, any ring homomorphism `f` from `R` to `S₁`, any function `s` from a type `σ` to natural numbers, and any element `a` of `R`, applying the function `MvPolynomial.map f` to the result of `MvPolynomial.monomial s a` is the same as first applying `f` to `a` and then applying `MvPolynomial.monomial s` to the result. In other words, it asserts the compatibility of monomial construction and polynomial map across rings.
More concisely: For any commutative semirings R and S₁, ring homomorphism f from R to S₁, function s : σ → ℕ, and element a in R, we have MvPolynomial.map f (MvPolynomial.monomial s a) = MvPolynomial.monomial s (f a).
|
MvPolynomial.eval₂_X
theorem MvPolynomial.eval₂_X :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(g : σ → S₁) (n : σ), MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n
The theorem `MvPolynomial.eval₂_X` states that for all types `R`, `S₁` and `σ` where `R` and `S₁` are commutative semirings, given a ring homomorphism `f` from `R` to `S₁`, a function `g` from `σ` to `S₁`, and an element `n` of type `σ`, evaluating the degree `1` monomial `MvPolynomial.X n` using the evaluation function `MvPolynomial.eval₂` with `f` and `g` yields the value `g n`. In mathematical terms, this means that applying the function `g` to the variable `n` gives the same result as evaluating the monomial $X_n$ where the coefficients are mapped according to `f` and the variables are mapped according to `g`.
More concisely: For all commutative semirings R and S₁, ring homomorphism f : R → S₁, function g : σ → S₁, and element n : σ, we have MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n.
|
MvPolynomial.eval₂_mul
theorem MvPolynomial.eval₂_mul :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
{q : MvPolynomial σ R} (f : R →+* S₁) (g : σ → S₁) {p : MvPolynomial σ R},
MvPolynomial.eval₂ f g (p * q) = MvPolynomial.eval₂ f g p * MvPolynomial.eval₂ f g q
The theorem `MvPolynomial.eval₂_mul` states that for any commutative semirings `R` and `S₁` with `f` being a ring homomorphism from `R` to `S₁` and `g` being a function from the index set of the variables to `S₁`, for any multivariate polynomials `p` and `q` over `R`, the evaluation of the product `p * q` using the evaluation function `eval₂` is equal to the product of the evaluations of `p` and `q` individually. In other words, the evaluation function `eval₂` preserves multiplication of multivariate polynomials.
More concisely: For any commutative semirings R and S₁, ring homomorphism f from R to S₁, and multivariate polynomials p and q over R, we have eval₂(p * q) = eval₂(p) * eval₂(q).
|
MvPolynomial.map_X
theorem MvPolynomial.map_X :
∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
(n : σ), (MvPolynomial.map f) (MvPolynomial.X n) = MvPolynomial.X n
The theorem `MvPolynomial.map_X` states that for any commutative semirings `R` and `S₁`, and any ring homomorphism `f` from `R` to `S₁`, and any `n` in the index set `σ`, mapping the polynomial `X_n` (which is a degree `1` monomial) under `f` using the function `MvPolynomial.map` results in the same `X_n`. In other words, the mapping preserves the degree `1` monomial `X_n`.
More concisely: For any commutative semirings R and S₁, and ring homomorphism f from R to S₁, the degree 1 monomial X\_n in R is mapped to X\_n under the function MvPolynomial.map from R-polynomials to S₁-polynomials by f.
|