Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.not_even_one

Modification history

2019-07-13 16:25

src/data/nat/parity.lean

feat(data/{nat,int}/parity): the 'even' predicate on nat and int (#1219) …

Added nat.not_even_one View on Github →