Skip to content

Commit

Permalink
chore: add shortcut instances after LinearOrder Nat (#19346)
Browse files Browse the repository at this point in the history
This prevents Lean from going through the Lattice structure, which requires additional imports.
  • Loading branch information
Ruben-VandeVelde committed Nov 22, 2024
1 parent 2bb0410 commit af19119
Show file tree
Hide file tree
Showing 7 changed files with 13 additions and 8 deletions.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Prime/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ import Mathlib.Algebra.Group.Even
import Mathlib.Algebra.Group.Units.Equiv
import Mathlib.Algebra.GroupWithZero.Hom
import Mathlib.Algebra.Prime.Defs
import Mathlib.Order.Lattice
import Mathlib.Order.Monotone.Basic

/-!
# Associated, prime, and irreducible elements.
Expand Down
1 change: 0 additions & 1 deletion Mathlib/CategoryTheory/Functor/OfSequence.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ Copyright (c) 2024 Joël Riou. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joël Riou
-/
import Mathlib.Algebra.Order.Group.Nat
import Mathlib.CategoryTheory.Category.Preorder
import Mathlib.CategoryTheory.EqToHom

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/Int/GCD.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ import Mathlib.Algebra.Group.Int
import Mathlib.Algebra.GroupWithZero.Semiconj
import Mathlib.Algebra.Group.Commute.Units
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Order.Lattice
import Mathlib.Data.Set.Operations
import Mathlib.Order.Basic
import Mathlib.Order.Bounds.Defs

/-!
Expand Down
7 changes: 7 additions & 0 deletions Mathlib/Data/Nat/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,13 @@ instance instLinearOrder : LinearOrder ℕ where
decidableLE := inferInstance
decidableEq := inferInstance

-- Shortcut instances
instance : Preorder ℕ := inferInstance
instance : PartialOrder ℕ := inferInstance
instance : Min ℕ := inferInstance
instance : Max ℕ := inferInstance
instance : Ord ℕ := inferInstance

instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩

@[simp] theorem default_eq_zero : default = 0 := rfl
Expand Down
6 changes: 3 additions & 3 deletions Mathlib/Data/Nat/Log.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ Copyright (c) 2020 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Yaël Dillies
-/
import Mathlib.Order.Interval.Set.Defs
import Mathlib.Order.Monotone.Basic
import Mathlib.Tactic.Bound.Attribute
import Mathlib.Tactic.Monotonicity.Attr
import Mathlib.Order.Lattice
import Mathlib.Tactic.Contrapose
import Mathlib.Order.Interval.Set.Defs
import Mathlib.Tactic.Monotonicity.Attr

/-!
# Natural number logarithms
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/Nat/Prime/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
import Batteries.Data.Nat.Gcd
import Mathlib.Algebra.Prime.Defs
import Mathlib.Algebra.Ring.Nat
import Mathlib.Order.Lattice
import Mathlib.Order.Basic

/-!
# Prime numbers
Expand Down
1 change: 0 additions & 1 deletion Mathlib/Data/Nat/Size.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
import Mathlib.Data.Nat.Bits
import Mathlib.Order.Lattice

/-! Lemmas about `size`. -/

Expand Down

0 comments on commit af19119

Please sign in to comment.