Documentation

Mathlib.Data.Nat.Factorial.BigOperators

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.prod_factorial_pos {α : Type u_1} (s : Finset α) (f : α) :
0 < is, (f i).factorial
theorem Nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : Finset α) (f : α) :
is, (f i).factorial (∑ is, f i).factorial
theorem Nat.descFactorial_eq_prod_range (n : ) (k : ) :
n.descFactorial k = iFinset.range k, (n - i)