Polynomial.derivative_C
theorem Polynomial.derivative_C :
∀ {R : Type u} [inst : Semiring R] {a : R}, Polynomial.derivative (Polynomial.C a) = 0
The theorem `Polynomial.derivative_C` states that for any semiring `R` and any element `a` of `R`, the formal derivative of the constant polynomial `a` is `0`. In other words, when we compute the derivative of a polynomial that is simply a constant (with no variable term), the result is always zero, which aligns with our understanding from basic calculus.
More concisely: For any semiring R and any constant polynomial f(x) = a in R[x], its derivative f'(x) equals 0.
|
Polynomial.derivative_add
theorem Polynomial.derivative_add :
∀ {R : Type u} [inst : Semiring R] {f g : Polynomial R},
Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
The theorem `Polynomial.derivative_add` states that for all types `R` equipped with a semiring structure `[inst : Semiring R]`, and for any two polynomials `f` and `g` over this type, the derivative of the sum of `f` and `g` is equal to the sum of the derivatives of `f` and `g`. In mathematical notation, this can be written as: for all `f, g ∈ Polynomial R`, `(f + g)' = f' + g'`. This theorem is a formalization of the standard result from calculus that the derivative of a sum of functions is equal to the sum of their derivatives.
More concisely: The theorem `Polynomial.derivative_add` asserts that the derivative of the sum of two polynomials is equal to the sum of their derivatives.
|
Polynomial.derivative_monomial
theorem Polynomial.derivative_monomial :
∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ),
Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * ↑n)
The theorem `Polynomial.derivative_monomial` states that for any semiring `R`, and for any element `a` of `R` and non-negative integer `n`, the derivative of the monomial `a * X^n` (represented in Lean as `(Polynomial.monomial n) a`) is `(a * n) * X^(n - 1)` (represented in Lean as `(Polynomial.monomial (n - 1)) (a * ↑n)`). This corresponds to the standard rule for differentiating a monomial in calculus.
More concisely: The theorem asserts that the derivative of the monomial `a * X^n` in a polynomial over a semiring is equal to `(a * n) * X^(n - 1)`.
|
Polynomial.derivative_X
theorem Polynomial.derivative_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative Polynomial.X = 1
The theorem `Polynomial.derivative_X` states that for any type `R` that is a semiring, the derivative of the polynomial `Polynomial.X` is equal to 1. In other words, taking the formal derivative of the polynomial variable (also known as indeterminate), which is simply the polynomial \(X\), yields 1. This corresponds to the well-known calculus rule that the derivative of \(x\) with respect to \(x\) is 1.
More concisely: The derivative of the polynomial indeterminate (Polynomial.X) is equal to 1, for any semiring type R.
|
Polynomial.derivative_pow
theorem Polynomial.derivative_pow :
∀ {R : Type u} [inst : CommSemiring R] (p : Polynomial R) (n : ℕ),
Polynomial.derivative (p ^ n) = Polynomial.C ↑n * p ^ (n - 1) * Polynomial.derivative p
The theorem `Polynomial.derivative_pow` states that for any commutative semiring `R`, any polynomial `p` over `R`, and any natural number `n`, the derivative of the `n`-th power of `p` is equal to `n` times the `n-1`-th power of `p` times the derivative of `p`. In mathematical notation, this is saying that if `p` is a polynomial and `n` a natural number, then the derivative of `p^n` is `n*p^{n-1}*p'`, where `p'` is the derivative of `p`. This is a formalization of the power rule for derivatives in the context of polynomials.
More concisely: The derivative of a polynomial `p` raised to the power of `n` is equal to `n * p^(n-1) * p'`.
|
Polynomial.derivative_apply
theorem Polynomial.derivative_apply :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R),
Polynomial.derivative p = p.sum fun n a => Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
The theorem `Polynomial.derivative_apply` states that for any semiring `R` and any polynomial `p` over `R`, the derivative of `p` is equivalent to summing the results of a function applied to the coefficients of the polynomial `p`. This function multiplies each coefficient `a` by its corresponding power `n`, converts the product to a constant polynomial via the `Polynomial.C` function and then multiplies it by `X` raised to the power `(n - 1)`. In other words, it is carrying out the formal derivative of a polynomial, where each term `aX^n` is transformed to `naX^(n-1)`.
More concisely: For any semiring `R` and polynomial `p` over `R`, the derivative of `p` is equal to the sum of the polynomials obtained by multiplying each coefficient `a` of `p` by `X^(n-1)` and raising `X` to the power `n`, where `n` is the degree of the corresponding term, and summing these polynomials over all terms in `p`.
|
Polynomial.coeff_derivative
theorem Polynomial.coeff_derivative :
∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
(Polynomial.derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
The theorem `Polynomial.coeff_derivative` states that for any semiring `R`, given any polynomial `p` from `R` and a natural number `n`, the coefficient of `X^n` in the derivative of `p` is equal to the coefficient of `X^(n+1)` in `p` multiplied by `(n+1)`. In other words, if `p` is a polynomial, then the coefficient of the `n`-th term in the derivative of `p` is the same as the coefficient of the `(n+1)`-th term in `p`, scaled by `(n+1)`. This corresponds to the power rule of differentiation in calculus.
More concisely: The coefficient of the `n`-th term in the derivative of a polynomial `p` equals the coefficient of `X^(n+1)` in `p`, multiplied by `(n+1)`.
|
Polynomial.derivative_mul
theorem Polynomial.derivative_mul :
∀ {R : Type u} [inst : Semiring R] {f g : Polynomial R},
Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
The theorem `Polynomial.derivative_mul` states that for any type `R` that is a semiring and for any polynomials `f` and `g` over `R`, the derivative of the product of `f` and `g` is equal to the product of the derivative of `f` and `g` plus the product of `f` and the derivative of `g`. This is equivalent to the product rule in calculus, stated as `(f*g)' = f'*g + f*g'`.
More concisely: The derivative of the product of two polynomials over a semiring is equal to the sum of the product of the derivatives of each polynomial and the other polynomial.
|
Polynomial.derivative_sub
theorem Polynomial.derivative_sub :
∀ {R : Type u} [inst : Ring R] {f g : Polynomial R},
Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
The theorem `Polynomial.derivative_sub` states that for all types `R`, given a Ring structure on `R`, and for any two polynomials `f` and `g` with coefficients in `R`, the derivative of the difference of `f` and `g` is equal to the difference of the derivatives of `f` and `g`. In mathematical terms, this corresponds to the property (f - g)' = f' - g' for polynomials `f` and `g`, showing that the derivative operation in the polynomial ring respects subtraction.
More concisely: For all types `R` with a Ring structure and polynomials `f` and `g` over `R`, the derivative of `(f - g)` equals `(f' - g')`.
|
Polynomial.derivative_eval₂_C
theorem Polynomial.derivative_eval₂_C :
∀ {R : Type u} [inst : CommSemiring R] (p q : Polynomial R),
Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) =
Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q
This theorem is known as the Chain Rule for the formal derivative of polynomials. It states that for every commutative semiring `R` and for any two polynomials `p` and `q` over `R`, the derivative of the polynomial obtained by evaluating `p` at `q` (i.e., substituting `q` for the variable in `p`) is equal to the product of the derivative of `p` (after substituting `q` for the variable) and the derivative of `q`. In more mathematical terms, if we let `p` and `q` be polynomials, then the derivative of `p(q(x))` is `p'(q(x)) * q'(x)`, where `p'` is the derivative of `p`, `q'` is the derivative of `q`, and `x` is the variable.
More concisely: The derivative of a polynomial evaluated at another polynomial is equal to the product of the derivatives of both polynomials.
|
Polynomial.derivative_X_pow
theorem Polynomial.derivative_X_pow :
∀ {R : Type u} [inst : Semiring R] (n : ℕ),
Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C ↑n * Polynomial.X ^ (n - 1)
This theorem states that for any semiring `R` and any natural number `n`, the derivative of the polynomial `X` to the power `n` is equal to the constant polynomial of `n` times the polynomial `X` to the power `n - 1`. In mathematical terms, it expresses the familiar rule from calculus that the derivative of `x^n` is `n*x^{n-1}`, but here in the context of polynomials over a general semiring.
More concisely: For any semiring `R` and natural number `n`, the derivative of `X^n` is equal to `n * X^(n-1)`.
|
Polynomial.derivative_one
theorem Polynomial.derivative_one : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative 1 = 0
The theorem `Polynomial.derivative_one` states that for any semiring `R`, the derivative of a constant polynomial, specifically the polynomial `1`, is `0`. That is, when we take the derivative of the constant polynomial `1` (considered as a polynomial over any semiring `R`), the result is the zero polynomial.
More concisely: The derivative of the constant polynomial 1 over any semiring is the zero polynomial.
|
Polynomial.derivative_map
theorem Polynomial.derivative_map :
∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
The theorem `Polynomial.derivative_map` states that for any semirings `R` and `S`, and for any polynomial `p` over `R` and any ring homomorphism `f` from `R` to `S`, the derivative of the polynomial obtained by mapping `p` across `f` is equal to the mapping of the derivative of `p` across `f`. In other words, taking the derivative and then mapping is the same as mapping and then taking the derivative. This is a statement of the commutativity of the derivative operation with the map operation in the context of polynomials.
More concisely: For any semiring homomorphism between rings, the derivative of a polynomial mapped across the homomorphism is equal to the mapped derivative of the polynomial.
|