feat(NumberField/CanonicalEmbedding): Define the fundamental cone for the action of the units of a number field

[xroblot]

Let K be a number field of signature (r₁, r₂). This PR defines an action of the group of units (𝓞 K)ˣ of K on the space ℝ^r₁ × ℂ^r₂ via mixedEmbedding. The fundamental cone is a cone in ℝ^r₁ × ℂ^r₂ that is a fundamental domain for the action of (𝓞 K)ˣ up to roots of unity.

In a later PR #12333, we prove that points in the fundamental cone coming from (𝓞 K) are in a norm-preserving correspondence with the non-zero principal ideals of (𝓞 K) up to roots of unity.

---

• [x] depends on: #12249

[xroblot]

~~I changed this back to WIP because I think I might need to change a bit the definition of the fundamental cone.~~

[github-actions[bot]]

PR summary 5bb55bc729

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ basisUnitLattice + exists_unit_smul_mem + fundamentalCone + logEmbedding_fundSystem + mem_of_normAtPlace_eq + mixedEmbedding_apply_ofIsComplex + mixedEmbedding_apply_ofIsReal + normAtPlace_pos_of_mem + norm_pos_of_mem + smul_mem_iff_mem + smul_mem_of_mem + torsion_smul_mem_of_mem + unit_smul_mem_iff_mem_torsion

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.

[xroblot]

@riccardobrasca, this file is getting a bit long. Do you prefer that I break it into smaller PRs?

[riccardobrasca]

@riccardobrasca, this file is getting a bit long. Do you prefer that I break it into smaller PRs?

If you can yes. Feel free to ask for my review.

[xroblot]

@riccardobrasca, this file is getting a bit long. Do you prefer that I break it into smaller PRs?

If you can yes. Feel free to ask for my review.

All right, I will address @Ruben-VandeVelde review (Ruben, thanks for the review BTW!) and then split this PR.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12249~~
• ~~leanprover-community/mathlib4#13135~~
• ~~leanprover-community/mathlib4#16604~~
• ~~leanprover-community/mathlib4#16634~~
• ~~leanprover-community/mathlib4#16763~~ By Dependent Issues (🤖). Happy coding!

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

[riccardobrasca]

LGTM. If there is still something to be fixed we can do it later. Thanks!

bors merge

[bryangingechen]

This one seems to have fallen off the queue when bors crashed (not your fault). bors r+

Just in case something happens again: bors d+

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

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style