# 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) [] (a : ) (b : ) :
↑() = Polynomial.eval (a + 1) ()
theorem Nat.cast_descFactorial (S : Type u_1) [] (a : ) (b : ) :
↑() = Polynomial.eval (↑(a - (b - 1))) ()
theorem Nat.cast_factorial (S : Type u_1) [] (a : ) :
↑() = Polynomial.eval 1 ()
theorem Nat.cast_descFactorial_two (S : Type u_1) [Ring S] (a : ) :
↑() = a * (a - 1)

Convenience lemma. The a - 1 is not using truncated subtraction, as opposed to the definition of Nat.descFactorial as a natural.