Documentation

Mathlib.Data.Nat.Factorial.Cast

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)
theorem Nat.cast_descFactorial_two (S : Type u_1) [Ring S] (a : ) :
(a.descFactorial 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.