theorem
Int.not_prime_of_int_mul
{a : ℤ}
{b : ℤ}
{c : ℕ}
(ha : 1 < Int.natAbs a)
(hb : 1 < Int.natAbs b)
(hc : a * b = ↑c)
:
theorem
Int.Prime.dvd_natAbs_of_coe_dvd_sq
{p : ℕ}
(hp : Nat.Prime p)
(k : ℤ)
(h : ↑p ∣ k ^ 2)
:
p ∣ Int.natAbs k