Documentation Verification Report

BigOperators

📁 Source: Mathlib/Data/Nat/Factorial/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_range_add_one_eq_factorial`, `ascFactorial_eq_prod_range`, `descFactorial_eq_prod_range`, `factorial_coe_dvd_prod`, `factorial_eq_prod_range_add_one`, `monotone_factorial`, `prod_factorial_dvd_factorial_sum`, `prod_factorial_pos`	8
Total	8

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_range_add_one_eq_factorial` 📖	mathematical	—	`prod` `Nat.instCommMonoid` `range` `Nat.factorial`	—	`Nat.factorial_eq_prod_range_add_one`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ascFactorial_eq_prod_range` 📖	mathematical	—	`ascFactorial` `Finset.prod` `instCommMonoid` `Finset.range`	—	`ascFactorial.eq_2` `Finset.prod_range_succ_comm`
`descFactorial_eq_prod_range` 📖	mathematical	—	`descFactorial` `Finset.prod` `instCommMonoid` `Finset.range`	—	`descFactorial.eq_2` `Finset.prod_range_succ_comm`
`factorial_coe_dvd_prod` 📖	mathematical	—	`factorial` `Finset.prod` `Int.instCommMonoid` `Finset.range`	—	`Finset.prod_int_mod` `Finset.prod_congr` `factorial_ne_zero` `factorial_dvd_ascFactorial` `ascFactorial_eq_prod_range` `Finset.prod_natCast` `cast_add`
`factorial_eq_prod_range_add_one` 📖	mathematical	—	`factorial` `Finset.prod` `instCommMonoid` `Finset.range`	—	`factorial.eq_2` `Finset.prod_range_succ_comm`
`monotone_factorial` 📖	mathematical	—	`Monotone` `instPreorder` `factorial`	—	`factorial_le`
`prod_factorial_dvd_factorial_sum` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `factorial` `Finset.sum` `instAddCommMonoid`	—	`Finset.cons_induction_on` `Finset.prod_cons` `Finset.sum_cons` `Dvd.dvd.trans` `mul_dvd_mul_left` `factorial_mul_factorial_dvd_factorial_add`
`prod_factorial_pos` 📖	mathematical	—	`Finset.prod` `instCommMonoid` `factorial`	—	`Finset.prod_pos` `instZeroLEOneClass` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `instNontrivial` `factorial_pos`

---

← Back to Index