Factorial

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

Statistics

Metric	Count
Definitions	0
Theorems coprime_descFactorial_of_lt_of_le, coprime_factorial_of_lt, dvd_factorial, coprime_factorial_iff	4
Total	4

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_factorial_iff 📖	mathematical	—	factorial minFac	—	not_le iff_not_comm Prime.not_coprime_iff_dvd minFac_prime minFac_dvd dvd_factorial minFac_pos le_trans minFac_le_of_dvd Prime.two_le Prime.dvd_factorial

Nat.Prime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprime_descFactorial_of_lt_of_le 📖	mathematical	Nat.Prime	Nat.descFactorial	—	Nat.descFactorial_eq_div coprime_factorial_of_lt
coprime_factorial_of_lt 📖	mathematical	Nat.Prime	Nat.factorial	—	coprime_iff_not_dvd dvd_factorial not_le
dvd_factorial 📖	mathematical	Nat.Prime	Nat.factorial	—	not_dvd_one not_le_of_gt pos Nat.factorial_succ dvd_mul lt_or_eq_of_le dvd_refl

---

← Back to Index