mathlib documentation

data.nat.associated

source
theorem nat.prime_iff {p : ℕ} :
nat.prime p ↔ prime p

source
theorem nat.irreducible_iff_prime {p : ℕ} :
irreducible p ↔ prime p