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
to ↑a - 1, the other factor is 0 anyway.
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)
Convenience lemma. The a - 1 is not using truncated subtraction, as opposed to the definition
of nat.desc_factorial as a natural.