Lemmas about nat.prime using `int`s #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem int.not_prime_of_int_mul {a b : ℤ} {c : ℕ} (ha : 1 < a.nat_abs) (hb : 1 < b.nat_abs) (hc : a * b = ↑c) :

theorem int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul {p : ℕ} (p_prime : nat.prime p) {m n : ℤ} {k l : ℕ} (hpm : ↑(p ^ k) ∣ m) (hpn : ↑(p ^ l) ∣ n) (hpmn : ↑(p ^ (k + l + 1)) ∣ m * n) :

↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n

theorem int.prime.dvd_nat_abs_of_coe_dvd_sq {p : ℕ} (hp : nat.prime p) (k : ℤ) (h : ↑p ∣ k ^ 2) :

Lemmas about nat.prime using ints #