[Merged by Bors] - chore(FunctionField): rename vars when constant field is not nec. finite by xgenereux · Pull Request #37894 · leanprover-community/mathlib4

xgenereux · 2026-04-10T14:55:21Z

Asked by @MichaelStollBayreuth here.

I've also slightly adjusted the doc to reflect this.

I used the notation which I know from Rosen - Number Theory in Function Field.

github-actions · 2026-04-10T14:56:24Z

PR summary 05953fe9ce

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instance : IsDomain (ringOfIntegers F K)
+ instance : IsFractionRing (ringOfIntegers F K) K
+ instance : IsIntegralClosure (ringOfIntegers F K) F[X] K
+ instance : IsIntegrallyClosed (ringOfIntegers F K)
+ instance : Valuation.IsNontrivial (inftyValuation F) := ⟨RatFunc.X, by simp⟩
+ instance : Valuation.IsTrivialOn F (inftyValuation F)
+ instance [Algebra.IsSeparable (RatFunc F) K] : IsDedekindDomain (ringOfIntegers F K)
+ instance [Algebra.IsSeparable (RatFunc F) K] : IsNoetherian F[X] (ringOfIntegers F K)
+-+- algebraMap_injective
- instance : IsDomain (ringOfIntegers Fq F)
- instance : IsFractionRing (ringOfIntegers Fq F) F
- instance : IsIntegralClosure (ringOfIntegers Fq F) Fq[X] F
- instance : IsIntegrallyClosed (ringOfIntegers Fq F)
- instance : Valuation.IsNontrivial (inftyValuation Fq) := ⟨RatFunc.X, by simp⟩
- instance : Valuation.IsTrivialOn Fq (inftyValuation Fq)
- instance [Algebra.IsSeparable (RatFunc Fq) F] : IsDedekindDomain (ringOfIntegers Fq F)
- instance [Algebra.IsSeparable (RatFunc Fq) F] : IsNoetherian Fq[X] (ringOfIntegers Fq F)

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/NumberTheory/FunctionField.lean

MichaelStollBayreuth · 2026-04-10T15:25:08Z

Mathlib/NumberTheory/FunctionField.lean

-def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc Fq)
-deriving Field, Algebra (RatFunc Fq), Coe (RatFunc Fq), Inhabited
+/-- The completion `F((t⁻¹))` of `F(t)` with respect to the valuation at infinity. -/
+def _root_.FunctionField.FqtInfty := UniformSpace.Completion (RatFunc F)


Similarly here. InftyCompletionRatFunc?

But then this shouldn't be in this file right? I feel like the InftyValuation should be in the RatFunc folder no?

I guess so. (And at some point, it would make sense to move the current content of this file out of NumberTheory into FieldTheory. I think this place should be for material that is specifically about function fields over finite fields. But don't feel obliged to do that now, too!)

Would you like me to do this move in this PR or in another?
I am asking because all of these lemmas will have to change name (out of the FunctionField namespace) and will need to be deprecated.

It is probably cleaner to do that in a separate PR. In any case, thanks for doing this!

Mathlib/NumberTheory/FunctionField.lean

MichaelStollBayreuth

Looks good, modulo a few fixes in docstrings and fixing some names.

MichaelStollBayreuth · 2026-04-11T09:40:21Z

maintainer merge

github-actions · 2026-04-11T09:40:54Z

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

riccardobrasca · 2026-04-11T14:18:43Z

Thanks!

bors merge

@MichaelStollBayreuth

…ite (#37894) Asked by @MichaelStollBayreuth [here](#37447 (comment)). I've also slightly adjusted the doc to reflect this. I used the notation which I know from Rosen - Number Theory in Function Field. Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

mathlib-bors · 2026-04-11T14:31:06Z

Pull request successfully merged into master.

Build succeeded:

…c` namespace (#38030) From [this discussion](#37894 (comment)). Move `RatFunc` results from `FunctionField` field to `RatFunc` folder and namespace. Note : I used Claude Code to produce the deprecations. Co-authored-by: Xavier Genereux <xaviergenereux@hotmail.com>

xgenereux added 2 commits April 10, 2026 10:52

rename vars

b5398d9

adjust doc

17d95a2

xgenereux requested a review from MichaelStollBayreuth April 10, 2026 14:56

github-actions bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Apr 10, 2026

xgenereux mentioned this pull request Apr 10, 2026

feat(FunctionField): a function field is finite over Fq(y) for transcendental y #37447

Open

2 tasks

rename Fqt to Ft

792ff0b

MichaelStollBayreuth reviewed Apr 10, 2026

View reviewed changes

Mathlib/NumberTheory/FunctionField.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Apr 10, 2026

View reviewed changes

Mathlib/NumberTheory/FunctionField.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Apr 10, 2026

View reviewed changes

Mathlib/NumberTheory/FunctionField.lean Outdated Show resolved Hide resolved

MichaelStollBayreuth reviewed Apr 10, 2026

View reviewed changes

MichaelStollBayreuth added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 10, 2026

MichaelStollBayreuth self-assigned this Apr 10, 2026

suggested changes

c5d865f

xgenereux removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 10, 2026

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 11, 2026

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 11, 2026

mathlib-bors bot changed the title ~~chore(FunctionField): rename vars when constant field is not nec. finite~~ [Merged by Bors] - chore(FunctionField): rename vars when constant field is not nec. finite Apr 11, 2026

mathlib-bors bot closed this Apr 11, 2026

xgenereux mentioned this pull request Apr 14, 2026

[Merged by Bors] - chore(FunctionField): move inftyValuation and FqtInfty to RatFunc namespace #38030

Closed

Conversation

xgenereux commented Apr 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Apr 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 05953fe9ce

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

MichaelStollBayreuth Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

xgenereux Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

xgenereux Apr 10, 2026

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth Apr 11, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

MichaelStollBayreuth left a comment

Choose a reason for hiding this comment

Uh oh!

MichaelStollBayreuth commented Apr 11, 2026

Uh oh!

github-actions bot commented Apr 11, 2026

Uh oh!

riccardobrasca commented Apr 11, 2026

Uh oh!

mathlib-bors bot commented Apr 11, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

xgenereux commented Apr 10, 2026 •

edited

Loading

github-actions bot commented Apr 10, 2026 •

edited

Loading