Mathlib v3 is deprecated. Go to Mathlib v4

Theorem decidable.ne_or_eq

Modification history

2021-06-11 02:16
src/logic/basic.lean
chore(logic/basic): fixup `eq_or_ne` (#7865)
Modified decidable.ne_or_eqView on Github →
2021-05-15 21:20
src/logic/basic.lean
feat(data/logic/basic): `em.swap` and `eq_or_ne` (#7561)
Added decidable.ne_or_eqView on Github →