HepLean Documentation
Mathlib
.
Data
.
Nat
.
Prime
.
Factorial
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Nat.Factorial.Basic
Mathlib.Data.Nat.Prime.Defs
Imported by
Nat
.
Prime
.
dvd_factorial
Prime natural numbers and the factorial operator
#
source
theorem
Nat
.
Prime
.
dvd_factorial
{n p :
ℕ
}
:
Nat.Prime
p
→
(
p
∣
n
.factorial
↔
p
≤
n
)