Cast of factorials #
This file allows calculating factorials (including ascending and descending ones) as elements of a semiring.
This is particularly crucial for Nat.descFactorial 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.descFactorial 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_ascFactorial
(S : Type u_1)
[Semiring S]
(a : ℕ)
(b : ℕ)
:
↑(a.ascFactorial b) = Polynomial.eval (↑a) (ascPochhammer S b)
theorem
Nat.cast_descFactorial
(S : Type u_1)
[Semiring S]
(a : ℕ)
(b : ℕ)
:
↑(a.descFactorial b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)
theorem
Nat.cast_factorial
(S : Type u_1)
[Semiring S]
(a : ℕ)
:
↑a.factorial = Polynomial.eval 1 (ascPochhammer S a)
Convenience lemma. The a - 1 is not using truncated subtraction, as opposed to the definition
of Nat.descFactorial as a natural.