Theorem ne_of_ne_of_eq

Modification history

2024-04-19 20:51

Mathlib/Logic/Basic.lean

chore(Logic): reduce use of autoImplicit (#12135) …

Modified ne_of_ne_of_eq View on Github →

2024-02-20 23:51

Mathlib/Init/CCLemmas.lean

chore: Remove `Init.CCLemmas` (#10696) …

Modified ne_of_ne_of_eq View on Github →

2022-11-06 08:14

Mathlib/Init/CcLemmas.lean

feat: port init/cc_lemmas.lean (#532) …

Added ne_of_ne_of_eq View on Github →