English
Let p be a natural number. Then p is prime in the natural numbers if and only if its image as an integer is prime in the integers.
Русский
Пусть p — натуральное число. Тогда p простое в множестве натуральных чисел тогда и только тогда, когда его образ как целого числа прост в целых числах.
LaTeX
$$$\operatorname{Prime}_{\mathbb{N}}(p) \iff \operatorname{Prime}_{\mathbb{Z}}(p),$$$
Lean4
theorem prime_iff_prime_int {p : ℕ} : p.Prime ↔ _root_.Prime (p : ℤ) :=
⟨fun hp =>
⟨Int.natCast_ne_zero_iff_pos.2 hp.pos, mt Int.isUnit_iff_natAbs_eq.1 hp.ne_one, fun a b h =>
by
rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h
rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]⟩,
fun hp =>
Nat.prime_iff.2
⟨Int.natCast_ne_zero.1 hp.1, (mt Nat.isUnit_iff.1) fun h => by simp [h] at hp, fun a b => by
simpa only [Int.natCast_dvd_natCast, (Int.natCast_mul _ _).symm] using hp.2.2 a b⟩⟩
