prime_iff_natAbs_prime — Mathlib

English

An integer k is prime if and only if its absolute value is a prime natural number.

Русский

Целое число k простое тогда и только тогда, когда его абсолютное значение natAbs является простым числом натуралом.

LaTeX

$$$\\text{Prime}(k) \\iff \\text{Nat.Prime}(k.natAbs)$$$

Lean4

theorem prime_iff_natAbs_prime {k : ℤ} : Prime k ↔ Nat.Prime k.natAbs :=
  (Int.associated_natAbs k).prime_iff.trans Nat.prime_iff_prime_int.symm

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