Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.prime.not_dvd_one

Modification history

2022-03-15 06:38

src/data/nat/prime.lean

feat(algebra/associated): add irreducible.not_dvd_one (#12686)

Modified nat.prime.not_dvd_one View on Github →

2017-09-17 15:38

data/nat/prime.lean

feat(data/nat): better sqrt + pairing, prime numbers, renames...

Added nat.prime.not_dvd_one View on Github →