Derivation.compAEval_eq
theorem Derivation.compAEval_eq :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
[inst_6 : IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R),
(d.compAEval a) f = Polynomial.derivative f • (Module.AEval.of R M a) (d a)
This theorem is a form of the chain rule for derivatives, specialized for polynomials and derivations. Specifically, it states that if `f` is a polynomial over a commutative semiring `R`, and `d` is a derivation from `A` to `M` where `A` is also a commutative semiring and `M` is a module over `A` and `R`, then for any element `a` of `A`, the derivation of `f(a)` equals the derivative of `f` at `a`, times the derivation of `a`. The equation is expressed in the module `Module.AEval R M a` derived from `R[X]`. For the same equation in the module `M`, one should refer to `Derivation.compAEval_eq`.
More concisely: If `f` is a polynomial over a commutative semiring `R`, and `d` is a derivation from a commutative semiring `A` to an `R`-module `M`, then `d(f(a)) = d(f) * d(a)` for any `a` in `A`.
|
Polynomial.derivation_ext
theorem Polynomial.derivation_ext :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
[inst_3 : Module (Polynomial R) A] {D₁ D₂ : Derivation R (Polynomial R) A},
D₁ Polynomial.X = D₂ Polynomial.X → D₁ = D₂
The theorem `Polynomial.derivation_ext` states that for any two derivations `D₁` and `D₂` from the polynomial ring over a commutative semiring `R` to an `R`-module `A`, if these derivations coincide on the polynomial variable `X`, then `D₁` and `D₂` are identical. In other words, given the same commutative semiring, the same module, and the same polynomial variable, the derivation is uniquely determined by its action on the polynomial variable `X`.
More concisely: Given two derivations from a polynomial ring over a commutative semiring to an R-module, if they agree on the derivative of the polynomial variable X, then they are equal.
|
Derivation.comp_aeval_eq
theorem Derivation.comp_aeval_eq :
∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
[inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
[inst_6 : IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R),
d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) • d a
This theorem states a form of the chain rule for polynomials and derivations. If `f` is a polynomial over a commutative semiring `R`, `d` is a derivation from an `R`-algebra `A` to an `A`-module `M`, and `a` is an element of `A`, then the derivative of `f(a)` with respect to `d` is equal to `f'(a) * d(a)`, where `f'(a)` is the derivative of the polynomial `f` evaluated at `a`. The theorem asserts the equality in `M`. A corresponding version of this theorem exists for `Module.AEval R M a` in the function `Derivation.compAEval_eq`.
More concisely: The chain rule for polynomial derivations asserts that the derivative of a polynomial evaluated at an element, with respect to a derivation, equals the polynomial's derivative at that element multiplied by the derivation of the element.
|