Theorem exists_ne

Modification history

2023-09-06 06:13

Mathlib/Logic/Nontrivial/Defs.lean

chore: delay import of NeZero until after basic hierarchy (#6970)

Modified exists_ne View on Github →

2022-11-11 01:58

Mathlib/Logic/Nontrivial.lean

feat: port Mathlib.Logic.Nontrivial (#547) …

Added exists_ne View on Github →