mathlib documentation

data.int.nat_prime

Lemmas about nat.prime using ints

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