PowerSeries.coeff_derivativeFun
theorem PowerSeries.coeff_derivativeFun :
∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n : ℕ),
(PowerSeries.coeff R n) f.derivativeFun = (PowerSeries.coeff R (n + 1)) f * (↑n + 1)
This theorem states that for any commutative semiring `R` and any power series `f` over `R`, the `n`th coefficient of the formal derivative of `f` is equal to the `n+1`th coefficient of `f` times `n+1`. In other words, when we take the derivative of a power series, the coefficient of the `n`th term in the derivative is the same as the coefficient of the `(n+1)`th term in the original series, multiplied by `n+1`.
More concisely: For any commutative semiring `R` and power series `f` over `R`, the `n`th coefficient of the formal derivative of `f` equals `(n+1)` times the `(n+1)`th coefficient of `f`.
|
PowerSeries.derivative.ext
theorem PowerSeries.derivative.ext :
∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NoZeroSMulDivisors ℕ R] {f g : PowerSeries R},
(PowerSeries.derivative R) f = (PowerSeries.derivative R) g →
(PowerSeries.constantCoeff R) f = (PowerSeries.constantCoeff R) g → f = g
This theorem states that, for any commutative ring `R` with no zero `ℕ`-power smul divisors, if two formal power series `f` and `g` have the same constant term and the same derivative, then they are equal. In other words, if two formal power series over `R` share both their constant coefficient and their formal derivative, then the two series are identical.
More concisely: If `R` is a commutative ring with no zero `ℕ`-power smul divisors, then two formal power series `f` and `g` over `R` with equal constant terms and equal formal derivatives are equal.
|
PowerSeries.derivativeFun_C
theorem PowerSeries.derivativeFun_C :
∀ {R : Type u_1} [inst : CommSemiring R] (r : R), ((PowerSeries.C R) r).derivativeFun = 0
This theorem states that the derivative of a constant formal power series is zero. In other words, for any commutative semiring `R` and any element `r` of `R`, if we form the constant formal power series `r` (using the `PowerSeries.C` function) and then take its derivative (using `PowerSeries.derivativeFun`), the result is the zero power series. This is analogous to the fact in calculus that the derivative of a constant function is zero.
More concisely: The derivative of a constant formal power series over a commutative semiring is the zero power series.
|
PowerSeries.derivativeFun_mul
theorem PowerSeries.derivativeFun_mul :
∀ {R : Type u_1} [inst : CommSemiring R] (f g : PowerSeries R),
(f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun
This theorem states the Leibniz rule for the product of formal power series. Given a commutative semiring `R` and two power series `f` and `g` over `R`, the derivative of the product of `f` and `g` is equal to `f` times the derivative of `g` plus `g` times the derivative of `f`. In mathematical notation, if we denote the derivative of a power series `h` by `h'`, then this rule can be expressed as `(f * g)' = f * g' + g * f'`.
More concisely: The derivative of the product of two formal power series over a commutative semiring is equal to the sum of the product of the first series with the derivative of the second, and the product of the second series with the derivative of the first.
|