How to prove that a specific integer is irreducible

Stream: Is there code for X?

[Daniel Weber]

How do I prove Irreducible (47 : ℤ)? I know how to do it as a natural number, but I can't find lemmas for getting that as an integer

import Mathlib.Algebra.Associated.Basic
import Mathlib.Algebra.Group.Int
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Tactic.NormNum.Prime

example : Irreducible 47 := by rw [Nat.irreducible_iff_nat_prime]; norm_num

example : Irreducible (47 : ℤ) := by sorry

[Michael Stoll]

import Mathlib.RingTheory.Int.Basic
import Mathlib.Tactic.NormNum.Prime

example : Irreducible 47 := by rw [Nat.irreducible_iff_nat_prime]; norm_num

example : Irreducible (47 : ℤ) := by
  rw [irreducible_iff_prime, Int.prime_iff_natAbs_prime]
  norm_num

Note that there are more imports.

[Daniel Weber]

Thanks

[Michael Stoll]

(It turns out that the first two imports, even though listed by #min_imports, are not necessary. Edited the code above accordingly.)