instDecidablePredIrreducible — Mathlib

English

In ℤ, irreducible elements are decidable and correspond to primes; in particular, irreducible ⇔ prime.

Русский

В ℤ ирредуцируемые элементы разрешимы и соответствуют простым числам; то есть ирредуцируемость эквивалентна простоте.

LaTeX

$$$\\text{DecidablePred}(\\text{Irreducible}) = (\\text{Prime} \\Leftrightarrow \\text{Irreducible}).$$$

Lean4

instance (priority := 100) : DecidablePred (Irreducible : ℤ → Prop) := fun m ↦
  decidable_of_iff (Prime m) irreducible_iff_prime.symm

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