Theorem not_subsingleton

Modification history

2023-01-22 01:26

Mathlib/Logic/Nontrivial.lean

feat: `=`, `≠`, `<`, and `≤` functionality for `norm_num` (#1568) …

Modified not_subsingleton View on Github →

2022-11-11 01:58

Mathlib/Logic/Nontrivial.lean

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

Added not_subsingleton View on Github →