chore: Slightly modify the split of CanonicalEmbedding (#11917)

Create a new directory for the split of `CanonicalEmbedding` since more material is coming.

Also add some docstrings.

Mathlib.lean

@@ -3010,9 +3010,9 @@ import Mathlib.NumberTheory.ModularForms.SlashActions
 import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
 import Mathlib.NumberTheory.Multiplicity
 import Mathlib.NumberTheory.NumberField.Basic
-import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 import Mathlib.NumberTheory.NumberField.ClassNumber
-import Mathlib.NumberTheory.NumberField.ConvexBody
 import Mathlib.NumberTheory.NumberField.Discriminant
 import Mathlib.NumberTheory.NumberField.Embeddings
 import Mathlib.NumberTheory.NumberField.FractionalIdeal

Mathlib/NumberTheory/NumberField/ConvexBody.lean → Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

@@ -5,20 +5,33 @@ Authors: Xavier Roblot
 -/
 import Mathlib.MeasureTheory.Group.GeometryOfNumbers
 import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
-import Mathlib.NumberTheory.NumberField.CanonicalEmbedding
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
 
 #align_import number_theory.number_field.canonical_embedding from "leanprover-community/mathlib"@"60da01b41bbe4206f05d34fd70c8dd7498717a30"
 
 /-!
 # Convex Bodies
 
-This file contains theorems about convex bodies on infinite places of a number field.
+The file contains the definitions of several convex bodies lying in the space `ℝ^r₁ × ℂ^r₂`
+associated to a number field of signature `K` and proves several existence theorems by applying
+*Minkowski Convex Body Theorem* to those.
 
 ## Main definitions and results
 
-* `NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_lt`: let
-`f : InfinitePlace K → ℝ≥0`, if the product `∏ w, f w` is large enough, then there exists a
-nonzero algebraic integer `a` in `K` such that `w a < f w` for all infinite places `w`.
+* `NumberField.mixedEmbedding.convexBodyLT`: The set of points `x` such that `‖x w‖ < f w` for all
+infinite places `w` with `f : InfinitePlace K → ℝ≥0`.
+
+* `NumberField.mixedEmbedding.convexBodySum`: The set of points `x` such that
+`∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B`
+
+* `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_lt`: Let `I` be a fractional ideal of `K`.
+Assume that `f` is such that `minkowskiBound K I < volume (convexBodyLT K f)`, then there exists a
+nonzero algebraic number `a` in `I` such that `w a < f w` for all infinite places `w`.
+
+* `NumberField.mixedEmbedding.exists_ne_zero_mem_ideal_of_norm_le`: Let `I` be a fractional ideal
+of `K`. Assume that `B` is such that `minkowskiBound K I < volume (convexBodySum K B)` (see
+`convexBodySum_volume` for the computation of this volume), then there exists a nonzero algebraic
+number `a` in `I` such that `|Norm a| < (B / d) ^ d` where `d` is the degree of `K`.
 
 ## Tags
 
@@ -31,6 +44,7 @@ namespace NumberField.mixedEmbedding
 
 open NumberField NumberField.InfinitePlace FiniteDimensional
 
+/-- The space `ℝ^r₁ × ℂ^r₂` with `(r₁, r₂)` the signature of `K`. -/
 local notation "E" K =>
   ({w : InfinitePlace K // IsReal w} → ℝ) × ({w : InfinitePlace K // IsComplex w} → ℂ)
 
@@ -582,6 +596,11 @@ theorem exists_primitive_element_lt_of_isComplex {w₀ : InfinitePlace K} (hw₀
       rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
       set_option tactic.skipAssignedInstances false in norm_num
 
+/-- Let `I` be a fractional ideal of `K`. Assume that `B : ℝ` is such that
+`minkowskiBound K I < volume (convexBodySum K B)` where `convexBodySum K B` is the set of points
+`x` such that `∑ w real, ‖x w‖ + 2 * ∑ w complex, ‖x w‖ ≤ B` (see `convexBodySum_volume` for
+the computation of this volume), then there exists a nonzero algebraic number `a` in `I` such
+that `|Norm a| < (B / d) ^ d` where `d` is the degree of `K`. -/
 theorem exists_ne_zero_mem_ideal_of_norm_le {B : ℝ}
     (h : (minkowskiBound K I) ≤ volume (convexBodySum K B)) :
     ∃ a ∈ (I : FractionalIdeal (𝓞 K)⁰ K), a ≠ 0 ∧
@@ -623,3 +642,5 @@ theorem exists_ne_zero_mem_ringOfIntegers_of_norm_le {B : ℝ}
   exact ⟨a, ha, h_nz, h_bd⟩
 
 end minkowski
+
+end NumberField.mixedEmbedding

Mathlib/NumberTheory/NumberField/Discriminant.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.Data.Real.Pi.Bounds
-import Mathlib.NumberTheory.NumberField.ConvexBody
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 
 /-!
 # Number field discriminant

Mathlib/NumberTheory/NumberField/Units.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.LinearAlgebra.Matrix.Gershgorin
-import Mathlib.NumberTheory.NumberField.ConvexBody
+import Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
 import Mathlib.NumberTheory.NumberField.Norm
 import Mathlib.RingTheory.RootsOfUnity.Basic