mathlib3 documentation


Factorial with big operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.big_operators.basic leads to a cyclic import.

theorem nat.prod_factorial_pos {α : Type u_1} (s : finset α) (f : α ) :
0 < (λ (i : α), (f i).factorial)
theorem nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : finset α) (f : α ) : (λ (i : α), (f i).factorial) (s.sum (λ (i : α), f i)).factorial