Factorial with big operators

This file contains some lemmas on factorials in combination with big operators.

While in terms of semantics they could be in the Basic.lean file, importing Algebra.BigOperators.Group.Finset leads to a cyclic import.

theorem Nat.monotone_factorial : Monotone factorial

theorem Nat.prod_factorial_pos {α : Type u_1} (s : Finset α) (f : α → ℕ) : 0 < ∏ i ∈ s, (f i).factorial

theorem Nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : Finset α) (f : α → ℕ) : ∏ i ∈ s, (f i).factorial ∣ (∑ i ∈ s, f i).factorial

theorem Nat.factorial_eq_prod_range_add_one (n : ℕ) : n.factorial = ∏ i ∈ Finset.range n, (i + 1)

@[simp]

theorem Finset.prod_range_add_one_eq_factorial (n : ℕ) : ∏ i ∈ range n, (i + 1) = n.factorial

theorem Nat.ascFactorial_eq_prod_range (n k : ℕ) : n.ascFactorial k = ∏ i ∈ Finset.range k, (n + i)

theorem Nat.descFactorial_eq_prod_range (n k : ℕ) : n.descFactorial k = ∏ i ∈ Finset.range k, (n - i)

theorem Nat.factorial_coe_dvd_prod (k : ℕ) (n : ℤ) : ↑k.factorial ∣ ∏ i ∈ Finset.range k, (n + ↑i)

k! divides the product of any k consecutive integers.