MvPolynomial.bind₂_X_right
theorem MvPolynomial.bind₂_X_right :
∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
(f : R →+* MvPolynomial σ S) (i : σ), (MvPolynomial.bind₂ f) (MvPolynomial.X i) = MvPolynomial.X i
The theorem `MvPolynomial.bind₂_X_right` states that, for any types `σ`, `R`, and `S` with `R` and `S` being commutative semirings, and given a function `f` mapping from `R` to `MvPolynomial σ S` and any `i` of type `σ`, applying the function `MvPolynomial.bind₂ f` to the degree `1` monomial `MvPolynomial.X i` (in the multivariate polynomial ring over `R` indexed by `σ`) results in the same degree `1` monomial `MvPolynomial.X i`. In other words, the bind operation `MvPolynomial.bind₂` preserves the degree `1` monomials in the polynomial ring over `σ`.
More concisely: For any commutative semirings R and S, and a function f from R to MvPolynomial (over σ and S), the application of MvPolynomial.bind₂ f to the degree 1 monomial X i in the polynomial ring over σ results in the same degree 1 monomial X i.
|
MvPolynomial.map_bind₁
theorem MvPolynomial.map_bind₁ :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
(f : R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
(MvPolynomial.map f) ((MvPolynomial.bind₁ g) φ) =
(MvPolynomial.bind₁ fun i => (MvPolynomial.map f) (g i)) ((MvPolynomial.map f) φ)
The theorem `MvPolynomial.map_bind₁` states that for any commutative semiring `R` and `S`, a ring homomorphism `f` from `R` to `S`, a function `g` from an arbitrary type `σ` to multivariate polynomials over `R` indexed by another arbitrary type `τ`, and a multivariate polynomial `φ` over `R` indexed by `σ`, if we first map the polynomial `φ` through `g` and then apply the `f` map to the result, it is the same as first applying the `f` map to `φ` and `g(i)` for each index `i`, and then mapping `φ` through the resulting function. In other words, the operations of mapping a polynomial using a ring homomorphism and binding a polynomial via a function commute with each other.
More concisely: For any commutative semirings R and S, ring homomorphism f from R to S, function g from an arbitrary type σ to multivariate polynomials over R indexed by τ, and multivariate polynomial φ over R indexed by σ, the application of f to the polynomial obtained by mapping φ through g is equal to the polynomial obtained by mapping φ through the composition of g and the function that applies f to the image of g under each index i.
|
MvPolynomial.aeval_bind₁
theorem MvPolynomial.aeval_bind₁ :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
[inst_2 : Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
(MvPolynomial.aeval f) ((MvPolynomial.bind₁ g) φ) =
(MvPolynomial.aeval fun i => (MvPolynomial.aeval f) (g i)) φ
The theorem `MvPolynomial.aeval_bind₁` establishes a relationship between the evaluation of a multivariate polynomial and variable substitution in multivariate polynomials over an algebra.
More specifically, for any commutative semirings `R` and `S`, where `S` is an algebra over `R`, and for any types `σ` and `τ`, this theorem states that for any function `f: τ → S`, function `g: σ → MvPolynomial τ R`, and multivariate polynomial `φ: MvPolynomial σ R`, the evaluation of the result of substituting each variable in `φ` with the associated polynomial from `g` using the function `f` is equal to the evaluation of `φ` where each variable is substituted by the evaluation of the associated polynomial from `g` using `f`.
In other words, the order of performing variable substitution and evaluation in a multivariate polynomial does not matter. This property can be helpful while manipulating multivariate polynomials in algebraic structures.
More concisely: For any commutative semirings R and S, where S is an algebra over R, and for any functions f : τ -> S and g : σ -> MvPolynomial τ R, the evaluation of φ[g(x)] using x in σ, where φ is a multivariate polynomial in MvPolynomial σ R, is equal to the evaluation of φ evaluated at x, where each x in σ is substituted by g(x).
|
MvPolynomial.bind₁_X_right
theorem MvPolynomial.bind₁_X_right :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R) (i : σ),
(MvPolynomial.bind₁ f) (MvPolynomial.X i) = f i
The theorem `MvPolynomial.bind₁_X_right` states that for any types `σ`, `τ` and `R` where `R` has an instance of `CommSemiring`, for any function `f` mapping from `σ` to multivariate polynomials of `τ` and `R`, and for any `i` in `σ`, applying the "binding" operation `bind₁` on `f` and the degree `1` monomial `X_i` (represented by `MvPolynomial.X i`) results in the function `f` evaluated at `i`. Essentially, this theorem says that binding a multivariate polynomial function to a degree `1` monomial is equivalent to evaluating the function at the point represented by the monomial.
More concisely: For any type `σ`, `τ`, and commutative semiring `R`, and any function `f` mapping from `σ` to multivariate polynomials of `τ` and `R`, `bind₁(f) X_i = f i`, where `X_i` is the degree 1 monomial in the i-th variable and `bind₁` is the binding operation.
|
MvPolynomial.bind₂_C_right
theorem MvPolynomial.bind₂_C_right :
∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
(f : R →+* MvPolynomial σ S) (r : R), (MvPolynomial.bind₂ f) (MvPolynomial.C r) = f r
The theorem `MvPolynomial.bind₂_C_right` states that for any types `σ`, `R`, and `S` with `R` and `S` being commutative semirings, and for any ring homomorphism `f` from `R` to multivariate polynomials over `σ` and `S`, then binding `f` to the constant polynomial with value `r` in `R` results in the application of `f` to `r`. In other words, the bind operation on a constant multivariate polynomial effectively applies the ring homomorphism directly to the constant value.
More concisely: For any commutative semirings R and S, ring homomorphism f from R to multivariate polynomials over σ and S, and constant r in R, we have f (r) = bind₂ f (constant r).
|
MvPolynomial.bind₁_bind₁
theorem MvPolynomial.bind₁_bind₁ :
∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] {υ : Type u_6} (f : σ → MvPolynomial τ R)
(g : τ → MvPolynomial υ R) (φ : MvPolynomial σ R),
(MvPolynomial.bind₁ g) ((MvPolynomial.bind₁ f) φ) =
(MvPolynomial.bind₁ fun i => (MvPolynomial.bind₁ g) (f i)) φ
The theorem `MvPolynomial.bind₁_bind₁` states that for any types `σ`, `τ`, `υ`, and `R` with `R` being a commutative semiring, and for any functions `f : σ → MvPolynomial τ R`, `g : τ → MvPolynomial υ R`, and a multivariate polynomial `φ : MvPolynomial σ R`, the composition of the binding operation `bind₁` with `g` and then with `f` applied to φ is the same as the binding operation `bind₁` applied to the composition of `g` and `f` applied to each element `i`, then applied to `φ`.
In other words, this theorem assures the associativity property of the `bind₁` operation in the context of multivariate polynomials.
More concisely: For any commutative semiring R and multivariate polynomials φ : MvPolynomial σ R, f : σ → MvPolynomial τ R, and g : τ → MvPolynomial υ R, the binding operations bind₁(g)∘bind₁(f)(φ) and bind₁(g∘f)(φ) are equal.
|