Skip to content

Commit 7b2304f

Browse files
chore(NumberTheory/Height): move Instances.lean -> NumberField.lean (leanprover-community#34776)
This PR just changes the name of "Instances.lean" to "NumberField.lean". Rationale: I expect to add quite a number of number field specific results on heights eventually, and it makes sense to put them together with the `AdmissibleAbsValues` instance for number fields. Further instances for function fields can be added in a separate "FunctionField.lean" file at some later point. The module docstring will be updated in a follow-up PR.
1 parent fbfd573 commit 7b2304f

2 files changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5328,7 +5328,7 @@ public import Mathlib.NumberTheory.Harmonic.GammaDeriv
53285328
public import Mathlib.NumberTheory.Harmonic.Int
53295329
public import Mathlib.NumberTheory.Harmonic.ZetaAsymp
53305330
public import Mathlib.NumberTheory.Height.Basic
5331-
public import Mathlib.NumberTheory.Height.Instances
5331+
public import Mathlib.NumberTheory.Height.NumberField
53325332
public import Mathlib.NumberTheory.JacobiSum.Basic
53335333
public import Mathlib.NumberTheory.KummerDedekind
53345334
public import Mathlib.NumberTheory.LSeries.AbstractFuncEq
File renamed without changes.

0 commit comments

Comments
 (0)