Mathlib v3 is deprecated. Go to Mathlib v4

Theorem decidable.eq_or_ne

Modification history

2021-06-11 02:16

src/logic/basic.lean

chore(logic/basic): fixup `eq_or_ne` (#7865)

Modified decidable.eq_or_ne View on Github →

2021-05-15 21:20

src/logic/basic.lean

feat(data/logic/basic): `em.swap` and `eq_or_ne` (#7561)

Added decidable.eq_or_ne View on Github →