MvPolynomial.derivation_eqOn_supported
theorem MvPolynomial.derivation_eqOn_supported :
∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
[inst_2 : Module R A] [inst_3 : Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A}
{s : Set σ},
Set.EqOn (⇑D₁ ∘ MvPolynomial.X) (⇑D₂ ∘ MvPolynomial.X) s →
∀ {f : MvPolynomial σ R}, f ∈ MvPolynomial.supported R s → D₁ f = D₂ f
This theorem states that for any set `s` of variables (of type `σ`), any Commutative Semiring `R`, any Additive Commutative Monoid `A` that is also a module over `R` and `MvPolynomial σ R`, and any two derivations `D₁` and `D₂` from `MvPolynomial σ R` to `A`, if these derivations agree on the application of `MvPolynomial.X` (which represents the degree `1` monomial $X_n$) for every element in `s`, then they must agree on the result of any multivariate polynomial `f` which contains only the variables in the set `s` (i.e., `f` is in the subalgebra generated by `s`).
More concisely: If two derivations of multivariate polynomials agree on the application of degree 1 monomials for all variables in a set, they agree on the evaluation of any polynomial in the subalgebra generated by that set.
|
MvPolynomial.mkDerivation_X
theorem MvPolynomial.mkDerivation_X :
∀ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
[inst_2 : Module R A] [inst_3 : Module (MvPolynomial σ R) A] [inst_4 : IsScalarTower R (MvPolynomial σ R) A]
(f : σ → A) (i : σ), (MvPolynomial.mkDerivation R f) (MvPolynomial.X i) = f i
The theorem `MvPolynomial.mkDerivation_X` states that for any type `σ`, any type `R` with a commutative semiring structure, any type `A` with an additive commutative monoid structure, and which is an `R`-module and also a module over the multivariate polynomial type `MvPolynomial σ R`, and any function `f` from `σ` to `A`, and any element `i` of type `σ`, the result of applying the derivation `MvPolynomial.mkDerivation R f` to the degree `1` monomial `MvPolynomial.X i` is equal to `f i`. Here, `MvPolynomial.mkDerivation R f` is a derivation from the multivariate polynomial ring to `A`, and `MvPolynomial.X i` denotes the `i`-th variable in the multivariate polynomial ring.
More concisely: For any commutative semiring `R`, additive commutative monoid `A` that is an `R`-module and an `MvPolynomial σ R` module, function `f` from type `σ` to `A`, and element `i` of type `σ`, the derivative of the multivariate polynomial `MvPolynomial.X i` with respect to `f` equals `f i`.
|