Mathlib v3 is deprecated. Go to Mathlib v4

Theorem succ_ne_zero

Modification history

2017-09-19 02:55
data/encodable.lean
refactor(data/equiv,encodable): refactor/simplify proofs
Deleted succ_ne_zeroView on Github →
2017-09-08 20:06
data/encodable.lean
feat(data/encodable): ported data/encodable.lean from Lean2
Added succ_ne_zeroView on Github →