chore(FunctionField): rename vars when constant field is not nec. finite

[xgenereux]

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]

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).

[MichaelStollBayreuth]

Similarly here. InftyCompletionRatFunc?

[xgenereux]

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

[MichaelStollBayreuth]

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!)

[xgenereux]

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.

[MichaelStollBayreuth]

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