descPochhammer_succ_right
theorem descPochhammer_succ_right :
∀ (R : Type u) [inst : Ring R] (n : ℕ), descPochhammer R (n + 1) = descPochhammer R n * (Polynomial.X - ↑n) := by
sorry
The theorem `descPochhammer_succ_right` states that for any type `R` that forms a ring and any natural number `n`, the descending Pochhammer symbol of `n+1` is equal to the descending Pochhammer symbol of `n` multiplied by the polynomial `X - n`. In mathematical terms, the theorem says that the polynomial `X * (X - 1) * ... * (X - (n+1) + 1)` is the same as `((X * (X - 1) * ... * (X - n + 1)) * (X - n)`. This theorem shows the recursive property of the descending Pochhammer symbol in terms of polynomials.
More concisely: The descending Pochhammer symbol `(X-n)_n` equals `(X-n) * (X-n+1)_(n-1)` for any ring type `R` and natural number `n`.
|
ascPochhammer_eval_cast
theorem ascPochhammer_eval_cast :
∀ (S : Type u) [inst : Semiring S] (n k : ℕ),
↑(Polynomial.eval k (ascPochhammer ℕ n)) = Polynomial.eval (↑k) (ascPochhammer S n)
The theorem `ascPochhammer_eval_cast` states that for any semiring `S`, and any natural numbers `n` and `k`, the evaluation of the `ascPochhammer` polynomial with coefficients in the natural numbers, at `k`, cast to `S`, is equal to the evaluation of the `ascPochhammer` polynomial with coefficients in `S`, at `k` cast to `S`. In other words, it asserts the equality between the result of evaluating the ascending Pochhammer symbol (represented as a polynomial) when coefficients are in natural numbers and then cast into semiring `S`, and directly evaluating the ascending Pochhammer symbol in the semiring `S`.
More concisely: The theorem `ascPochhammer_eval_cast` asserts that the evaluation of the ascending Pochhammer polynomial with natural number coefficients in semiring `S`, and the direct evaluation of the ascending Pochhammer polynomial in `S`, are equal.
|
ascPochhammer_map
theorem ascPochhammer_map :
∀ {S : Type u} [inst : Semiring S] {T : Type v} [inst_1 : Semiring T] (f : S →+* T) (n : ℕ),
Polynomial.map f (ascPochhammer S n) = ascPochhammer T n
The theorem `ascPochhammer_map` states that for any two types `S` and `T`, both having a `Semiring` structure, any ring homomorphism `f` from `S` to `T`, and any natural number `n`, the action of mapping the ascending Pochhammer polynomial of `S` and `n` across the ring homomorphism `f` is equivalent to the ascending Pochhammer polynomial of `T` and `n`. In other words, the ring homomorphism `f` commutes with the ascending Pochhammer polynomial operation.
More concisely: Given types `S` and `T` with `Semiring` structures, a ring homomorphism `f` from `S` to `T`, and a natural number `n`, the ascending Pochhammer polynomials `(x + 1)^n` in `S` and `f((x + 1)^n)` in `T` are equal.
|
ascPochhammer_nat_eq_descFactorial
theorem ascPochhammer_nat_eq_descFactorial :
∀ (a b : ℕ), Polynomial.eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
The theorem `ascPochhammer_nat_eq_descFactorial` states that for all natural numbers `a` and `b`, the evaluation of the `ascPochhammer` polynomial at `a` is equal to the descending factorial of `a + b - 1` choose `b`. In other words, if you create a polynomial using `ascPochhammer` with `b` as the argument and then evaluate this polynomial at `a`, the result will be the same as taking the descending factorial of `a + b - 1` choose `b`. This establishes a connection between the evaluation of a certain class of polynomials and factorial operations.
More concisely: For all natural numbers `a` and `b`, `ascPochhammer a b = descFactorial (a + b - 1) Choices b`.
|
descPochhammer_map
theorem descPochhammer_map :
∀ {R : Type u} [inst : Ring R] {T : Type v} [inst_1 : Ring T] (f : R →+* T) (n : ℕ),
Polynomial.map f (descPochhammer R n) = descPochhammer T n
The theorem `descPochhammer_map` states that for every ring homomorphism `f` from a ring `R` to another ring `T` and for every natural number `n`, if you construct a `descPochhammer` polynomial with coefficients in `R` and then map it across the ring homomorphism `f` to `T` (using the `Polynomial.map` function), the result is the same as if you'd constructed the `descPochhammer` polynomial directly in `T`. In other words, the process of creating a `descPochhammer` polynomial commutes with the action of a ring homomorphism.
More concisely: For every ring homomorphism $f$ from a ring $R$ to another ring $T$ and every natural number $n$, the map $f$ applied to the descendant Pochhammer polynomial $P_{n}(X;a)$ in $R$ is equal to the descendant Pochhammer polynomial $P_{n}(X;a)$ constructed in $T$. In other words, $f(P_{n}(X;a)_{R}) = P_{n}(X;a)_{T}$.
|
ascPochhammer_nat_eq_ascFactorial
theorem ascPochhammer_nat_eq_ascFactorial : ∀ (n k : ℕ), Polynomial.eval n (ascPochhammer ℕ k) = n.ascFactorial k := by
sorry
The theorem `ascPochhammer_nat_eq_ascFactorial` states that for any two natural numbers `n` and `k`, the evaluation of the polynomial `ascPochhammer` at `n` with `k` as the degree of polynomial is equal to the ascending factorial of `n` and `k`. In other words, when the polynomial `X * (X + 1) * ... * (X + k - 1)` is evaluated at `X = n`, the result is the product of the series `n * (n + 1) * ... * (n + k - 1)`. This establishes a correspondence between the evaluation of the `ascPochhammer` polynomial and the ascending factorial computation.
More concisely: For any natural numbers `n` and `k`, the value of the polynomial `ascPochhammer X n k` evaluated at `X = n` equals the product `n * (n + 1) * ... * (n + k - 1)`.
|
descPochhammer_succ_left
theorem descPochhammer_succ_left :
∀ (R : Type u) [inst : Ring R] (n : ℕ),
descPochhammer R (n + 1) = Polynomial.X * (descPochhammer R n).comp (Polynomial.X - 1)
This theorem, `descPochhammer_succ_left`, states that for any natural number `n` and any type `R` that is a ring, the `descPochhammer` polynomial of `R` at `n + 1` is equal to the product of the polynomial `X` and the composition of the `descPochhammer` polynomial of `R` at `n` with the polynomial `X - 1`.
In other words, it expresses the computation of the `descPochhammer` polynomial at `n + 1` as an operation on the `descPochhammer` polynomial at `n`, using polynomial multiplication and composition. This allows us to inductively build up higher `descPochhammer` polynomials from lower ones.
More concisely: For any ring type R and natural number n, the descPochhammer polynomial of R at n+1 is equal to the product of X and the composition of the descPochhammer polynomial of R at n with the polynomial X - 1.
|
ascPochhammer_succ_left
theorem ascPochhammer_succ_left :
∀ (S : Type u) [inst : Semiring S] (n : ℕ),
ascPochhammer S (n + 1) = Polynomial.X * (ascPochhammer S n).comp (Polynomial.X + 1)
The theorem `ascPochhammer_succ_left` states that for any semiring `S` and natural number `n`, the ascending Pochhammer symbol of `S` at `(n + 1)` is equal to the polynomial `X` multiplied by the composition of the ascending Pochhammer symbol of `S` at `n` and the polynomial `X + 1`. The ascending Pochhammer symbol of `S` at `n` is the polynomial `X * (X + 1) * ... * (X + n - 1)` with coefficients in the semiring `S`.
More concisely: The ascending Pochhammer symbol of a semiring `S` at `n + 1` equals the product of `X`, the ascending Pochhammer symbol of `S` at `n`, and `(X + 1)` in `S[X]`.
|
descPochhammer_eval_eq_descFactorial
theorem descPochhammer_eval_eq_descFactorial :
∀ (R : Type u) [inst : Ring R] (n k : ℕ), Polynomial.eval (↑n) (descPochhammer R k) = ↑(n.descFactorial k) := by
sorry
The theorem `descPochhammer_eval_eq_descFactorial` states that for any type `R` with a ring structure and any natural numbers `n` and `k`, the evaluation of the `descPochhammer` polynomial of `k` with coefficients in `R` at `n` is equal to the descending factorial of `n` taken `k` at a time. In other words, if you construct the polynomial `X * (X - 1) * ... * (X - k + 1)` and substitute `n` for `X`, you get the same result as if you computed `n! / (n - k)!`. This connects the algebraic structure of a polynomial with the number theoretic concept of a factorial.
More concisely: For any ring `R` and natural numbers `n` and `k`, the evaluation of the `descPochhammer` polynomial of `k` with coefficients in `R` at `n` equals the descending factorial of `n` taken `k` at a time.
|
Mathlib.RingTheory.Polynomial.Pochhammer._auxLemma.1
theorem Mathlib.RingTheory.Polynomial.Pochhammer._auxLemma.1 :
∀ (S : Type u) [inst : Semiring S] (n k : ℕ),
Polynomial.eval (↑k) (ascPochhammer S n) = ↑(Polynomial.eval k (ascPochhammer ℕ n))
The theorem states that for any semiring `S` and any natural numbers `n` and `k`, the evaluation of the ascending Pochhammer polynomial `ascPochhammer S n` at `k` is equal to the evaluation of the ascending Pochhammer polynomial `ascPochhammer ℕ n` at `k`, when the result of the latter evaluation is coerced to `S`.
In more mathematical terms, this theorem states that evaluating the ascending Pochhammer polynomial of degree `n` at `k` is consistent across any semiring `S` and the semiring of natural numbers, `ℕ`, given that we proper cast the types.
More concisely: For any semiring `S` and natural numbers `n` and `k`, the evaluation of the ascending Pochhammer polynomial `ascPochhammer S n` at `k` equals the coerced evaluation of `ascPochhammer ℕ n` at `k`.
|
ascPochhammer_succ_right
theorem ascPochhammer_succ_right :
∀ (S : Type u) [inst : Semiring S] (n : ℕ), ascPochhammer S (n + 1) = ascPochhammer S n * (Polynomial.X + ↑n) := by
sorry
The theorem `ascPochhammer_succ_right` states that for any semiring `S` and any natural number `n`, the ascending Pochhammer symbol evaluated at `n + 1` is equal to the ascending Pochhammer symbol evaluated at `n` multiplied by the polynomial `X + n`. In mathematical terms, it expresses the relation `X * (X + 1) * ... * (X + n) = (X * (X + 1) * ... * (X + n - 1)) * (X + n)`, which is a property of the ascending Pochhammer symbol in the context of polynomial algebra.
More concisely: The ascending Pochhammer symbol evaluated at `n + 1` is equal to the product of the ascending Pochhammer symbol evaluated at `n` and the polynomial `X + n`.
|