English
Prime p iff p ≥ 2 and ∀ m, 2 ≤ m → m < p → ¬ m ∣ p.
Русский
Простое число p эквивалентно p ≥ 2 и ∀ m, 2 ≤ m → m < p → ¬ m ∣ p.
LaTeX
$$$\\\\mathrm{Prime}(p) \\\\iff 2 \\\\le p \\\\land \\\\forall m, 2 \\\\le m \\\\to m < p \\\\to \\\\neg m \\\\mid p$$$
Lean4
/-- This instance is set up to work in the kernel (`by decide`) for small values.
Below (`decidablePrime'`) we will define a faster variant to be used by the compiler
(e.g. in `#eval` or `by native_decide`).
If you need to prove that a particular number is prime, in any case
you should not use `by decide`, but rather `by norm_num`, which is
much faster.
-/
instance decidablePrime (p : ℕ) : Decidable (Prime p) :=
decidable_of_iff' _ prime_def_lt'
