Polynomial.hasseDeriv_apply
theorem Polynomial.hasseDeriv_apply :
∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (f : Polynomial R),
(Polynomial.hasseDeriv k) f = f.sum fun i r => (Polynomial.monomial (i - k)) (↑(i.choose k) * r)
The theorem `Polynomial.hasseDeriv_apply` states that for any semiring `R`, any natural number `k`, and any polynomial `f` with coefficients in `R`, the `k`th Hasse derivative of `f` is equal to the sum of the terms `(Polynomial.monomial (i - k)) (↑(Nat.choose i k) * r)`, where `i` ranges over the degrees of the monomials in `f`, `r` is the coefficient of the `i`th monomial in `f`, and `Nat.choose i k` is the binomial coefficient "i choose k". In other words, the `k`th Hasse derivative of a polynomial is obtained by multiplying each coefficient of the polynomial by the binomial coefficient "i choose k", and subtracting `k` from the degree of the corresponding term.
More concisely: The `k`th Hasse derivative of a polynomial `f` with coefficients in a semiring `R` is the sum of the terms `(i - k)! * r * x^(i)`, where `i` ranges over the degrees of the monomials in `f`, `r` is the coefficient of the `i`th monomial in `f`, and `x` is an indeterminate.
|
Polynomial.hasseDeriv_monomial
theorem Polynomial.hasseDeriv_monomial :
∀ {R : Type u_1} [inst : Semiring R] (k n : ℕ) (r : R),
(Polynomial.hasseDeriv k) ((Polynomial.monomial n) r) = (Polynomial.monomial (n - k)) (↑(n.choose k) * r)
This theorem states that for any semiring `R`, and any natural numbers `k` and `n`, and any element `r` of `R`, the `k`th Hasse derivative of the polynomial `a * X^n`, where `a` is `r`, is equal to the polynomial `b * X^(n-k)`, where `b` is the product of `r` and the binomial coefficient "n choose k". The Hasse derivative of a polynomial is a polynomial where the coefficient of `X^i` in the original polynomial is multiplied by the binomial coefficient "i choose k" and the power of `X` is reduced by `k`. The binomial coefficient "n choose k" is the number of ways to choose `k` elements from a set of `n` elements.
More concisely: For any semiring `R`, natural numbers `k` and `n`, and element `r` of `R`, the `k`th Hasse derivative of `r * X^n` is equal to `(r * binomialCoef n k) * X^(n-k)`.
|