BinomialRing.factorial_nsmul_multichoose
theorem BinomialRing.factorial_nsmul_multichoose :
∀ {R : Type u_1} [inst : Semiring R] [self : BinomialRing R] (r : R) (n : ℕ),
n.factorial • BinomialRing.multichoose r n = Polynomial.eval r (ascPochhammer R n)
The theorem `BinomialRing.factorial_nsmul_multichoose` states that for any type `R` that forms a semiring and a binomial ring, any element `r` of `R`, and any natural number `n`, the scalar multiplication of the factorial of `n` with the multichoose function evaluated at `r` and `n` equals the evaluation of the ascPochhammer polynomial at `r`. In other words, the value of the ascPochhammer polynomial of any `r` in the ring `R` at `n` is divisible by `n!`, where the quotient is given by the multichoose function. The ascPochhammer polynomial is defined as `X * (X + 1) * ... * (X + n - 1)`.
More concisely: For any semiring and binomial ring `R`, `(r : R)` being an element of `R`, and `n` being a natural number, `(n! * multichoose n r) * X ^ n = (ascPochhammer r X n)`.
|
BinomialRing.nsmul_right_injective
theorem BinomialRing.nsmul_right_injective :
∀ {R : Type u_1} [inst : Semiring R] [self : BinomialRing R] (n : ℕ), n ≠ 0 → Function.Injective fun x => n • x
The theorem `BinomialRing.nsmul_right_injective` states that in a binomial ring `R` that is a semiring, multiplication by a non-zero natural number `n` is an injective function. This means that if for any two elements `x` and `y` in the ring, the equality `n • x = n • y` (where `•` represents the multiplication operation defined in the ring) implies `x = y`.
More concisely: In a semiring `R` that is a binomial ring, multiplication by a non-zero natural number is an injective function. That is, for all `x` and `y` in `R`, if `n • x = n • y` then `x = y`.
|