instDecidablePredPrime — Mathlib

English

The primality predicate is decidable; primality of a natural number can be algorithmically determined.

Русский

Признак простоты разрешим; для каждого натурального числа можно эффективно определить простоту.

LaTeX

$$$\\\\operatorname{DecidablePred}(\\\\mathrm{Prime} : \\\\mathbb{N} \\\\to \\\\mathbf{Prop})$$$

Lean4

instance instDecidablePredPrime : DecidablePred (_root_.Prime : ℕ → Prop) := fun n ↦
  decidable_of_iff (Nat.Prime n) Nat.prime_iff

Похожие утверждения