Documentation

Mathlib.Data.Int.NatPrime

Lemmas about Nat.Prime using Ints #

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.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_natAbs_of_coe_dvd_sq {p : } (hp : Nat.Prime p) (k : ) (h : p k ^ 2) :