instDecidablePredPrime — Mathlib

English

There is a decidable predicate for primality on integers, reducing to natural primes via natAbs.

Русский

Существует разрешимое (решимое) свойство для простоты на числах ℤ, которое сводится к простоте натурального числа через natAbs.

LaTeX

$$$\\text{DecidablePred}(\\text{Prime}: \\mathbb{Z} \\to \\text{Prop}) = \\text{decidable_of_iff}(\\text{Nat.Prime}(-).)$$$

Lean4

instance instDecidablePredPrime : DecidablePred (Prime : ℤ → Prop) := fun m ↦
  decidable_of_iff (Nat.Prime m.natAbs) prime_iff_natAbs_prime.symm

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