Commit 2024-01-09 10:40 0c15e423

View on Github →

chore: shift Nat.ascFactorial down by one (#7965) change ascending factorial function Nat.ascFactorial to agree with mathematical literature. This means Nat.ascFactorial n k becomes n (n + 1) ⋯ (n + k - 1) instead of (n + 1) ⋯ (n + k)

Estimated changes

Modified Mathlib/Combinatorics/Derangements/Finite.lean

Modified Mathlib/Data/Nat/Choose/Basic.lean

added theorem Nat.ascFactorial_eq_factorial_mul_choose'

added theorem Nat.choose_eq_asc_factorial_div_factorial'

Modified Mathlib/Data/Nat/Factorial/Basic.lean

added theorem Nat.add_descFactorial_eq_ascFactorial'

modified theorem Nat.add_descFactorial_eq_ascFactorial

added theorem Nat.ascFactorial_eq_div'

modified theorem Nat.ascFactorial_eq_div

modified theorem Nat.ascFactorial_le_pow_add

modified theorem Nat.ascFactorial_lt_pow_add

modified theorem Nat.ascFactorial_of_sub

modified theorem Nat.ascFactorial_pos

modified theorem Nat.ascFactorial_succ

added theorem Nat.factorial_mul_ascFactorial'

modified theorem Nat.factorial_mul_ascFactorial

added theorem Nat.one_ascFactorial

modified theorem Nat.pow_lt_ascFactorial'

modified theorem Nat.pow_lt_ascFactorial

modified theorem Nat.pow_succ_le_ascFactorial

modified theorem Nat.zero_ascFactorial

Modified Mathlib/Data/Nat/Factorial/Cast.lean

modified theorem Nat.cast_ascFactorial

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/Tactic/Positivity/Basic.lean

Modified test/positivity.lean