mathlib3 documentation

data.nat.factorial.big_operators

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 < s.prod (λ (i : α), (f i).factorial)
theorem nat.prod_factorial_dvd_factorial_sum {α : Type u_1} (s : finset α) (f : α ) :
s.prod (λ (i : α), (f i).factorial) (s.sum (λ (i : α), f i)).factorial