Dvd

Statistics

Metric	Count
Definitions	0
Theorems `coprime_choose_of_lt`, `dvd_choose`, `dvd_choose_add`, `dvd_choose_self`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`coprime_choose_of_lt` 📖	mathematical	`Nat.Prime`	`Nat.choose`	—	`Nat.choose_eq_descFactorial_div_factorial` `coprime_descFactorial_of_lt_of_le` `Nat.factorial_dvd_descFactorial`
`dvd_choose` 📖	mathematical	`Nat.Prime`	`Nat.choose`	—	`LE.le.trans` `LT.lt.le` `dvd_choose_add`
`dvd_choose_add` 📖	mathematical	`Nat.Prime`	`Nat.choose`	—	`dvd_factorial` `dvd_mul` `Nat.choose_symm_add` `Nat.add_choose_mul_factorial_mul_factorial` `LT.lt.not_ge`
`dvd_choose_self` 📖	mathematical	`Nat.Prime`	`Nat.choose`	—	`dvd_choose` `LE.le.trans_lt` `le_rfl`

---