English
Nat.Prime p means that p is a prime number, i.e., an integer at least 2 whose only divisors are p and 1; this is witnessed by irreducibility.
Русский
Nat.Prime p означает, что p — простое число, то есть целое число не менее 2, единственными делителями которого являются p и 1; это фиксируется как irreducible.
LaTeX
$$$$ \text{Prime}(p) \iff \text{Irreducible}(p). $$$$
Lean4
/-- `Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number. -/
@[pp_nodot]
def Prime (p : ℕ) :=
Irreducible p
