Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fin.pos_iff_ne_zero

Modification history

2023-01-11 15:23
src/data/fin/basic.lean
refactor(data/fin/basic): fin refactor to use ne_zero (#18107)
Modified fin.pos_iff_ne_zeroView on Github →
2021-02-17 07:54
src/data/fin.lean
feat(data/fin): refactor `pred_above` (#6125) …
Added fin.pos_iff_ne_zeroView on Github →