We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 406d494 commit fd25822Copy full SHA for fd25822
1 file changed
Mathlib/Data/Nat/Basic.lean
@@ -39,13 +39,6 @@ instance instLinearOrder : LinearOrder ℕ where
39
toDecidableLE := inferInstance
40
toDecidableEq := inferInstance
41
42
--- Shortcut instances
43
-instance : Preorder ℕ := inferInstance
44
-instance : PartialOrder ℕ := inferInstance
45
-instance : Min ℕ := inferInstance
46
-instance : Max ℕ := inferInstance
47
-instance : Ord ℕ := inferInstance
48
-
49
instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩
50
51
attribute [gcongr] Nat.succ_le_succ Nat.div_le_div_right Nat.div_le_div_left Nat.div_le_div
0 commit comments