mathlib3 documentation

data.int.nat_prime

Lemmas about nat.prime using ints #

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) :