Skip to content

Commit e981638

Browse files
chore: move Northcott from NumberTheory.Height to Order (leanprover-community#39215)
Since the current module Mathlib.NumberTheory.Height.Northcott contains material that is not specific to heights (or number theory). we move it to Mathlib.Order.Northcott. This allows us to re-use the old module location to add a height-specific Northcott instance in a follow-up PR.
1 parent 686c76b commit e981638

5 files changed

Lines changed: 4 additions & 4 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5635,7 +5635,6 @@ public import Mathlib.NumberTheory.Harmonic.Int
56355635
public import Mathlib.NumberTheory.Harmonic.ZetaAsymp
56365636
public import Mathlib.NumberTheory.Height.Basic
56375637
public import Mathlib.NumberTheory.Height.MvPolynomial
5638-
public import Mathlib.NumberTheory.Height.Northcott
56395638
public import Mathlib.NumberTheory.Height.NumberField
56405639
public import Mathlib.NumberTheory.Height.Projectivization
56415640
public import Mathlib.NumberTheory.JacobiSum.Basic
@@ -6042,6 +6041,7 @@ public import Mathlib.Order.Monotone.Odd
60426041
public import Mathlib.Order.Monotone.Union
60436042
public import Mathlib.Order.Nat
60446043
public import Mathlib.Order.NonemptyFiniteChains
6044+
public import Mathlib.Order.Northcott
60456045
public import Mathlib.Order.Notation
60466046
public import Mathlib.Order.Nucleus
60476047
public import Mathlib.Order.OmegaCompletePartialOrder

Mathlib/GroupTheory/Descent.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module
88
public import Mathlib.Data.Real.Basic
99
public import Mathlib.GroupTheory.Finiteness
1010
public import Mathlib.GroupTheory.Index
11-
public import Mathlib.NumberTheory.Height.Northcott
11+
public import Mathlib.Order.Northcott
1212

1313
import Mathlib.Data.Set.Finite.Lemmas
1414
import Mathlib.Tactic.FieldSimp

Mathlib/NumberTheory/ArithmeticFunction/LFunction.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Thomas Browning
66
module
77

88
public import Mathlib.NumberTheory.ArithmeticFunction.Defs
9-
public import Mathlib.NumberTheory.Height.Northcott
9+
public import Mathlib.Order.Northcott
1010
public import Mathlib.RingTheory.PowerSeries.Basic
1111
public import Mathlib.RingTheory.PowerSeries.PiTopology
1212
public import Mathlib.RingTheory.PowerSeries.Substitution
File renamed without changes.

Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Xavier Roblot
66
module
77

88
public import Mathlib.Data.ZMod.QuotientRing
9-
public import Mathlib.NumberTheory.Height.Northcott
9+
public import Mathlib.Order.Northcott
1010
public import Mathlib.RingTheory.DedekindDomain.Basic
1111
public import Mathlib.RingTheory.IntegralDomain
1212
public import Mathlib.RingTheory.Ideal.Norm.AbsNorm

0 commit comments

Comments
 (0)