feat(NumberField/CanonicalEmbedding): put an euclidean space structure on the mixed space

[xroblot]

This PR defines the natural euclidian space stucture on the mixed space ℝ^r₁ × ℂ^r₂ of a number field of signature of K and the map between the Euclidean.mixedSpace K and mixedSpace. Proves many properties of this map. In particular, it is volume preserving.

This PR is part of the proof of the Analytic Class Number Formula.

---

[github-actions[bot]]

PR summary eaaa9e06f5

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	2282	2284	+2 (+0.09%)

Import changes for all files

Files

Import difference

12 files Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

2

---

Declarations diff

+ finrank + instance : BorelSpace (euclidean.mixedSpace K) := ⟨rfl⟩ + instance : DiscreteTopology (euclidean.integerLattice K) := by + instance : IsZLattice ℝ (euclidean.integerLattice K) := by + instance : MeasurableSpace (euclidean.mixedSpace K) := borel _ + instance : Nontrivial (euclidean.mixedSpace K) := (toMixed K).toEquiv.nontrivial + instance : Ring (euclidean.mixedSpace K) + integerLattice + mixedSpace + stdOrthonormalBasis + stdOrthonormalBasis_map_eq + toMixed + volumePreserving_toMixed + volumePreserving_toMixed_symm

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.

[riccardobrasca]

Part of this is PR is also in #18234, right?

[xroblot]

Part of this is PR is also in #18234, right?

Sorry. I forgot to finish cleaning up before removing WIP. Let me put it back for the time being.

(I am getting a bit lost with all these PRs open at the same time 😅 )

[riccardobrasca]

Part of this is PR is also in #18234, right?

Sorry. I forgot to finish cleaning up before removing WIP. Let me put it back for the time being.

(I am getting a bit lost with all these PRs open at the same time 😅 )

OK, let's merge the other one, so the diff will become smaller (modulo conflicts).

[mathlib-bors[bot]]

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

[xroblot]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style