[Merged by Bors] - chore: Slightly modify the split of CanonicalEmbedding

Mathlib.lean

@@ -3008,9 +3008,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/CanonicalEmbedding.lean → Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -507,5 +507,3 @@ theorem mem_span_fractionalIdealLatticeBasis (x : (E K)) :
   rfl
 
 end integerLattice
-
-end NumberField.mixedEmbedding

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
+# Canonical embedding of a number field
 
-This file contains theorems about convex bodies on infinite places of a number field.
+The canonical embedding of a number field `K` of degree `n` is the ring homomorphism
+`K →+* ℂ^n` that sends `x ∈ K` to `(φ_₁(x),...,φ_n(x))` where the `φ_i`'s are the complex
+embeddings of `K`. Note that we do not choose an ordering of the embeddings, but instead map `K`
+into the type `(K →+* ℂ) → ℂ` of `ℂ`-vectors indexed by the complex embeddings.
 
-## Main definitions and results
+## Main 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.exists_ne_zero_mem_ideal_lt`: Let `I` be a fractional ideal of `K`.
+Assume that `f : InfinitePlace K → ℝ≥0` is such that
+`minkowskiBound K I < volume (convexBodyLT K f)` where `convexBodyLT K f` is the set of
+points `x` such that `‖x w‖ < f w` for all infinite places `w` (see `convexBodyLT_volume` for
+the computation of this volume), 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)` 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`.
 
 ## 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