Theorems · Theorem · number theory
Nat.prod_factorial_dvd_factorial_sum
∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), ∏ i ∈ s, (f i).factorial ∣ (∑ i ∈ s, f i).factorial- Defined in
- Mathlib.Data.Nat.Factorial.BigOperators
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- Finset.sumstatement and proof · cited by 5,195
- Finset.prodstatement and proof · cited by 2,356
- Nat.factorialstatement and proof · cited by 616
- Finset.consproof · cited by 221
- Dvd.dvd.transproof · cited by 148
- Finset.sum_consproof · cited by 84
- Finset.prod_consproof · cited by 60
- Finset.cons_induction_onproof · cited by 37
- mul_dvd_mul_leftproof · cited by 34
- Nat.factorial_mul_factorial_dvd_factorial_addproof · cited by 3
Cited by5
Results whose statement or proof uses this declaration.
- Nat.multinomial_specproof · cited by 4
- Nat.multinomial_consproof · cited by 3
- Nat.multinomial_insert_oneproof · cited by 1
- Nat.multinomial_posproof · cited by 0
- Nat.multinomial_two_mul_le_mul_multinomialproof · cited by 0