[Merged by Bors] - feat(NumberTheory/NumberField/FinitePlaces): the finite places of a number field

[fbarroero]

This file defines finite places of a number field K as absolute values coming from an embedding
into a completion of K associated to a non-zero prime ideal of 𝓞 K with some basic APIs.

This is part of a project which aims to define heights. The next step is the product formula.

---

[github-actions]

PR summary 4e978f3c00

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.NumberField.FinitePlaces (new file)	2402

---

Declarations diff

+ FinitePlace
+ FinitePlace.mk
+ FinitePlace.norm_def
+ FinitePlace.norm_def'
+ FinitePlace.norm_def_int
+ apply
+ embedding
+ instNormedFieldValuedAdicCompletion
+ instRankOneValuedAdicCompletion
+ instance : FunLike (FinitePlace K) K ℝ
+ instance : MonoidWithZeroHomClass (FinitePlace K) K ℝ
+ instance : NonnegHomClass (FinitePlace K) K ℝ
+ maximalIdeal
+ maximalIdeal_inj
+ maximalIdeal_injective
+ maximalIdeal_mk
+ mk_eq_iff
+ mk_maximalIdeal
+ mulSupport_finite
+ mulSupport_finite_int
+ norm_embedding_eq
+ norm_eq_one_iff_not_mem
+ norm_le_one
+ norm_lt_one_iff_mem
+ one_lt_norm
+ pos_iff
+ toNNReal_Valued_eq_vadicAbv
+ vadicAbv
+ vadicAbv_def

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

[fbarroero]

Thank you @MichaelStollBayreuth for the review and the suggestions!

[MichaelStollBayreuth]

Looks good to me now!
maintainer merge

[github-actions]

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

[kbuzzard]

Thanks a lot! Just to flag that in the FLT project we are also thinking about this sort of thing; in particular this file https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HaarMeasure/DistribHaarChar.lean defines the norm on the units of any locally compact topological field as being the factor which Haar measure is scaled by under multiplication. What we need in FLT is the assertion that if B is a f.d. central simple algebra over a number field K, then multiplication by a unit in B doesn't change Haar measure on B tensor_K A_K. This is a generalization of what your goal is here so we should take care not to duplicate work. See for example ImperialCollegeLondon/FLT#223 .

bors merge

[kbuzzard]

Remark: this could have just been w.1.pos_iff

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[fbarroero]

Thanks a lot! Just to flag that in the FLT project we are also thinking about this sort of thing; in particular this file https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/HaarMeasure/DistribHaarChar.lean defines the norm on the units of any locally compact topological field as being the factor which Haar measure is scaled by under multiplication. What we need in FLT is the assertion that if B is a f.d. central simple algebra over a number field K, then multiplication by a unit in B doesn't change Haar measure on B tensor_K A_K. This is a generalization of what your goal is here so we should take care not to duplicate work. See for example ImperialCollegeLondon/FLT#223 .

bors merge

Thanks!
I see what you mean. I am planning to PR the Product Formula soon. My goal is to define the Weil height, you don't need that for FLT, do you?