# 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 : ℕ)
:

↑(Nat.ascFactorial a b) = Polynomial.eval (↑a + 1) (ascPochhammer S b)

theorem
Nat.cast_descFactorial
(S : Type u_1)
[Semiring S]
(a : ℕ)
(b : ℕ)
:

↑(Nat.descFactorial a b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)

theorem
Nat.cast_factorial
(S : Type u_1)
[Semiring S]
(a : ℕ)
:

↑(Nat.factorial a) = Polynomial.eval 1 (ascPochhammer S a)

theorem
Nat.cast_descFactorial_two
(S : Type u_1)
[Ring S]
(a : ℕ)
:

↑(Nat.descFactorial a 2) = ↑a * (↑a - 1)

Convenience lemma. The `a - 1`

is not using truncated subtraction, as opposed to the definition
of `Nat.descFactorial`

as a natural.