Skip to content

[Merged by Bors] - chore: move Northcott from NumberTheory.Height to Order#39215

Closed
MichaelStollBayreuth wants to merge 1 commit into
leanprover-community:masterfrom
MichaelStollBayreuth:MS_move_Northcott_0
Closed

[Merged by Bors] - chore: move Northcott from NumberTheory.Height to Order#39215
MichaelStollBayreuth wants to merge 1 commit into
leanprover-community:masterfrom
MichaelStollBayreuth:MS_move_Northcott_0

Conversation

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

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.


Open in Gitpod

@MichaelStollBayreuth MichaelStollBayreuth added t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-order Order theory labels May 11, 2026
@github-actions
Copy link
Copy Markdown

PR summary f40a8e8c6e

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.Height.Northcott -592
Mathlib.Order.Northcott 592

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.


No changes to strong technical debt.
No changes to weak technical debt.

note: file Mathlib/NumberTheory/Height/Northcott.lean` was renamed to `Mathlib/Order/Northcott.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!

@github-actions github-actions Bot added the file-removed A Lean module was (re)moved without a `deprecated_module` annotation label May 11, 2026
@faenuccio
Copy link
Copy Markdown
Contributor

Thanks!

bors d=tb65536

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 11, 2026

✌️ tb65536 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 11, 2026
@tb65536
Copy link
Copy Markdown
Contributor

tb65536 commented May 11, 2026

bors r+

(usually we would add a deprecation, but this will get resolved in a few days hopefully)

mathlib-bors Bot pushed a commit that referenced this pull request May 11, 2026
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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors Bot commented May 11, 2026

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: move Northcott from NumberTheory.Height to Order [Merged by Bors] - chore: move Northcott from NumberTheory.Height to Order May 11, 2026
@mathlib-bors mathlib-bors Bot closed this May 11, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-order Order theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants