Cast of factorials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file allows calculating factorials (including ascending and descending ones) as elements of a semiring.
This is particularly crucial for
nat.desc_factorial as subtraction on
ℕ does not correspond
to subtraction on a general semiring. For example, we can't rely on existing cast lemmas to prove
↑(a.desc_factorial 2) = ↑a * (↑a - 1). We must use the fact that, whenever
↑(a - 1) is not equal
↑a - 1, the other factor is
theorem nat.cast_asc_factorial (S : Type u_1) [semiring S] (a b : ℕ) :
↑(a.asc_factorial b) = polynomial.eval (↑a + 1) (pochhammer S b)
theorem nat.cast_desc_factorial (S : Type u_1) [semiring S] (a b : ℕ) :
↑(a.desc_factorial b) = polynomial.eval ↑(a - (b - 1)) (pochhammer S b)
theorem nat.cast_factorial (S : Type u_1) [semiring S] (a : ℕ) :
↑(a.factorial) = polynomial.eval 1 (pochhammer S a)
theorem nat.cast_desc_factorial_two (S : Type u_1) [ring S] (a : ℕ) :
Convenience lemma. The
a - 1 is not using truncated subtraction, as opposed to the definition
nat.desc_factorial as a natural.