mathlib documentation

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.desc_factorial as substraction on does not correspond to substraction 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 : ) :
theorem nat.cast_desc_factorial (S : Type u_1) [semiring S] (a b : ) :
theorem nat.cast_factorial (S : Type u_1) [semiring S] (a : ) :
theorem nat.cast_desc_factorial_two (S : Type u_1) [ring S] (a : ) :
(a.desc_factorial 2) = (a) * (a - 1)

Convenience lemma. The a - 1 is not using truncated substraction, as opposed to the definition of nat.desc_factorial as a natural.