@[reducible, inline]

abbrev GeometryOfNumbers.IsCocompactAddSubgroup {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] (H : AddSubgroup G) : Prop

@[reducible, inline]

abbrev GeometryOfNumbers.IsFullLattice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Prop

theorem GeometryOfNumbers.discrete_full_rank_iff_zlattice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Module.finrank ℤ ↥L = Module.finrank ℝ E ↔ IsZLattice ℝ L

theorem GeometryOfNumbers.measure_image_linearMap {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (T : E →ₗ[ℝ] E) (S : Set E) : μ (⇑T '' S) = ENNReal.ofReal |LinearMap.det T| * μ S

@[reducible, inline]

abbrev GeometryOfNumbers.IsFundamentalDomain {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] (L : Submodule ℤ E) (F : Set E) (μ : MeasureTheory.Measure E := by volume_tac) : Prop

theorem GeometryOfNumbers.fundamental_domain_measure_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {F : Set E} (hF : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) : ZLattice.covolume L μ = μ.real F

@[reducible, inline]

noncomputable abbrev GeometryOfNumbers.covol {E : Type u_1} [NormedAddCommGroup E] [MeasurableSpace E] (L : Submodule ℤ E) (μ : MeasureTheory.Measure E := by volume_tac) : ℝ

theorem GeometryOfNumbers.covol_sublattice {ι : Type u_1} [Fintype ι] (Λ' Λ : Submodule ℤ (ι → ℝ)) [DiscreteTopology ↥Λ'] [IsZLattice ℝ Λ'] [DiscreteTopology ↥Λ] [IsZLattice ℝ Λ] (h : Λ' ≤ Λ) : ZLattice.covolume Λ' MeasureTheory.volume = ↑(Λ'.toAddSubgroup.relIndex Λ.toAddSubgroup) * ZLattice.covolume Λ MeasureTheory.volume

def GeometryOfNumbers.IsSymmetricSet {V : Type u_1} [AddCommGroup V] (S : Set V) : Prop

theorem GeometryOfNumbers.minkowski_lattice_point {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {L : AddSubgroup E} [Countable ↥L] {F : Set E} (hF : MeasureTheory.IsAddFundamentalDomain (↥L) F μ) {S : Set E} (h_symm : ∀ x ∈ S, -x ∈ S) (h_conv : Convex ℝ S) (h_meas : μ F * 2 ^ Module.finrank ℝ E < μ S) : ∃ (x : ↥L), x ≠ 0 ∧ ↑x ∈ S

theorem GeometryOfNumbers.covol_ring_of_integers (K : Type u_1) [Field K] [NumberField K] : ZLattice.covolume (NumberField.mixedEmbedding.integerLattice K) MeasureTheory.volume = 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.discr K)|

Alias of NumberField.mixedEmbedding.covolume_integerLattice.

theorem GeometryOfNumbers.covol_fractional_ideal (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ZLattice.covolume (NumberField.mixedEmbedding.idealLattice K I) MeasureTheory.volume = ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ NumberField.InfinitePlace.nrComplexPlaces K * √|↑(NumberField.discr K)|

Alias of NumberField.mixedEmbedding.covolume_idealLattice.

theorem GeometryOfNumbers.minkowski_bound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) : ∃ a ∈ ↑I, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) a| ≤ ↑(FractionalIdeal.absNorm ↑I) * (4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K * ↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K * √|↑(NumberField.discr K)|

@[reducible, inline]

abbrev GeometryOfNumbers.convexBody (K : Type u_1) [Field K] [NumberField K] (t : ℝ) : Set (NumberField.mixedEmbedding.mixedSpace K)

theorem GeometryOfNumbers.convex_body_volume (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) = ↑(NumberField.mixedEmbedding.convexBodySumFactor K) * ENNReal.ofReal B ^ Module.finrank ℚ K

Alias of NumberField.mixedEmbedding.convexBodySum_volume.

theorem GeometryOfNumbers.finite_ideals_bounded_norm (K : Type u_1) [Field K] [NumberField K] (M : ℕ) : {I : Ideal (NumberField.RingOfIntegers K) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ M}.Finite

theorem GeometryOfNumbers.normalizedFactors_card_le_log (K : Type u_1) [Field K] [NumberField K] (I : Ideal (NumberField.RingOfIntegers K)) (hI : I ≠ ⊥) (M : ℕ) (hIM : Ideal.absNorm I ≤ M) : (UniqueFactorizationMonoid.normalizedFactors I).card ≤ Nat.log 2 M

theorem GeometryOfNumbers.prime_ideals_bounded_norm_card_lt (K : Type u_1) [Field K] [NumberField K] (M : ℕ) (hM : M ≠ 0) : Nat.card ↑{𝔭 : Ideal (NumberField.RingOfIntegers K) | 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ Ideal.absNorm 𝔭 ≤ M} + 1 ≤ Module.finrank ℚ K * M

theorem GeometryOfNumbers.ideals_bounded_norm_card_le (K : Type u_1) [Field K] [NumberField K] (M : ℕ) : Nat.card ↑{I : Ideal (NumberField.RingOfIntegers K) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ M} ≤ (Module.finrank ℚ K * M) ^ Nat.log 2 M

theorem GeometryOfNumbers.class_group_finite_integral_closure (A : Type u_1) [EuclideanDomain A] [Infinite A] [DecidableEq A] (K : Type u_2) [Field K] [Algebra A K] [IsFractionRing A K] (L : Type u_3) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] (B : Type u_4) [CommRing B] [IsDomain B] [Algebra A B] [Algebra B L] [IsFractionRing B L] [Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [IsIntegralClosure B A L] {abv : AbsoluteValue A ℤ} (adm : abv.IsAdmissible) : Finite (ClassGroup B)

theorem GeometryOfNumbers.discr_lower_bound (K : Type u_1) [Field K] [NumberField K] : ↑(Module.finrank ℚ K) ^ (2 * Module.finrank ℚ K) / ((4 / Real.pi) ^ (2 * NumberField.InfinitePlace.nrComplexPlaces K) * ↑(Module.finrank ℚ K).factorial ^ 2) ≤ ↑|NumberField.discr K|

Alias of NumberField.abs_discr_ge'.

---

The Minkowski lower bound n^{2n}/((4/pi)^{2r_2}*n!^2) for the absolute value of the discriminant of a number field of degree n.

theorem GeometryOfNumbers.discr_abs_gt_one {K : Type u_1} [Field K] [NumberField K] (h : 1 < Module.finrank ℚ K) : 1 < |NumberField.discr K|

theorem GeometryOfNumbers.finite_numberfields_of_bounded_discr (A : Type u_2) [Field A] [CharZero A] (N : ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | |NumberField.discr ↥↑K| ≤ ↑N}.Finite

Alias of NumberField.finite_of_discr_bdd.

---

Hermite Theorem. Let N be an integer. There are only finitely many number fields (in some fixed extension of ℚ) of discriminant bounded by N.

theorem GeometryOfNumbers.different_ideal_bounds (A : Type u_1) (K : Type u_2) (L : Type u_3) (B : Type u_4) [CommRing A] [IsDomain A] [IsDedekindDomain A] [Field K] [Algebra A K] [IsFractionRing A K] [Field L] [Algebra A L] [CommRing B] [IsDedekindDomain B] [Algebra B L] [IsFractionRing B L] [Algebra A B] [Algebra K L] [IsScalarTower A B L] [IsScalarTower A K L] [Module.IsTorsionFree A B] [Module.Finite A B] [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] (𝔮 : Ideal B) [𝔮.IsPrime] (h𝔮 : 𝔮 ≠ ⊥) (𝔭 : Ideal A) [𝔭.IsMaximal] [𝔮.LiesOver 𝔭] (hsep : Algebra.IsSeparable (A ⧸ 𝔭) (B ⧸ 𝔮)) : have e := 𝔭.ramificationIdx 𝔮; ↑(e - 1) ≤ emultiplicity 𝔮 (differentIdeal A B) ∧ emultiplicity 𝔮 (differentIdeal A B) ≤ ↑(e - 1) + emultiplicity 𝔮 (Ideal.span {↑e}) ∧ (emultiplicity 𝔮 (differentIdeal A B) = ↑(e - 1) ↔ ¬ringChar (A ⧸ 𝔭) ∣ e)

theorem GeometryOfNumbers.norm_valuation_discr_le (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] : have 𝔭 := Ideal.span {↑p}; emultiplicity (↑p) (NumberField.discr K) ≤ ↑(∑ P ∈ primesOverFinset 𝔭 (NumberField.RingOfIntegers K), 𝔭.inertiaDeg P * (emultiplicity P (differentIdeal ℤ (NumberField.RingOfIntegers K))).toNat)

theorem GeometryOfNumbers.different_upper_bound_numberfield (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) (hP : P ∈ primesOverFinset (Ideal.span {↑p}) (NumberField.RingOfIntegers K)) : have 𝔭 := Ideal.span {↑p}; have e := 𝔭.ramificationIdx P; emultiplicity P (differentIdeal ℤ (NumberField.RingOfIntegers K)) ≤ ↑(e - 1) + emultiplicity P (Ideal.span {↑e})

theorem GeometryOfNumbers.emultiplicity_span_natCast_eq (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) (hP : P ∈ primesOverFinset (Ideal.span {↑p}) (NumberField.RingOfIntegers K)) (n : ℕ) (hn : n ≠ 0) : have 𝔭 := Ideal.span {↑p}; emultiplicity P (Ideal.span {↑n}) = ↑(𝔭.ramificationIdx P * padicValNat p n)

theorem GeometryOfNumbers.different_valuation_le (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] (P : Ideal (NumberField.RingOfIntegers K)) (hP : P ∈ primesOverFinset (Ideal.span {↑p}) (NumberField.RingOfIntegers K)) : have 𝔭 := Ideal.span {↑p}; (emultiplicity P (differentIdeal ℤ (NumberField.RingOfIntegers K))).toNat ≤ 𝔭.ramificationIdx P - 1 + 𝔭.ramificationIdx P * padicValNat p (𝔭.ramificationIdx P)

theorem GeometryOfNumbers.discr_emultiplicity_le_sum_ramification_aux (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] : have 𝔭 := Ideal.span {↑p}; emultiplicity (↑p) (NumberField.discr K) ≤ ↑(∑ P ∈ primesOverFinset 𝔭 (NumberField.RingOfIntegers K), 𝔭.inertiaDeg P * (𝔭.ramificationIdx P - 1 + 𝔭.ramificationIdx P * padicValNat p (𝔭.ramificationIdx P)))

theorem GeometryOfNumbers.sum_reindex_fin {α : Type u_1} {β : Type u_2} [AddCommMonoid β] (S : Finset α) (g : α → β) : ∑ x ∈ S, g x = ∑ i : Fin S.card, g ↑(S.equivFin.symm i)

theorem GeometryOfNumbers.discr_emultiplicity_le_sum_ramification (K : Type u_1) [Field K] [NumberField K] (p : ℕ) [Fact (Nat.Prime p)] : ∃ (ι : Type) (S : Finset ι) (e : ι → ℕ) (f : ι → ℕ), S.Nonempty ∧ (∀ i ∈ S, 1 ≤ e i) ∧ (∀ i ∈ S, 1 ≤ f i) ∧ ∑ i ∈ S, e i * f i = Module.finrank ℚ K ∧ emultiplicity (↑p) (NumberField.discr K) ≤ ↑(∑ i ∈ S, f i * (e i - 1 + e i * padicValNat p (e i)))

theorem GeometryOfNumbers.sum_ramification_padic_le {ι : Type u_1} (S : Finset ι) (e f : ι → ℕ) (p n : ℕ) (he : ∀ i ∈ S, 1 ≤ e i) (hf : ∀ i ∈ S, 1 ≤ f i) (hS : S.Nonempty) (hsum : ∑ i ∈ S, e i * f i = n) : ∑ i ∈ S, f i * (e i - 1 + e i * padicValNat p (e i)) ≤ n * Nat.log p n + n - 1

theorem GeometryOfNumbers.discr_padic_val_bound (K : Type u) [Field K] [NumberField K] (p : ℕ) [hp : Fact (Nat.Prime p)] : emultiplicity (↑p) (NumberField.discr K) ≤ ↑(Module.finrank ℚ K) * ↑(Nat.log p (Module.finrank ℚ K)) + ↑(Module.finrank ℚ K) - 1

def GeometryOfNumbers.IsUnramifiedOutside (K : Type u_1) [Field K] [NumberField K] (S : Finset ℕ) : Prop

theorem GeometryOfNumbers.isUnramifiedOutside_filter_prime {K : Type u_1} [Field K] [NumberField K] {S : Finset ℕ} : IsUnramifiedOutside K S ↔ IsUnramifiedOutside K (Finset.filter Nat.Prime S)

theorem GeometryOfNumbers.discr_bdd_of_unramified_outside (K : Type u) [Field K] [NumberField K] (n : ℕ) (hn : Module.finrank ℚ K = n) (S : Finset ℕ) (hSp : ∀ p ∈ S, Nat.Prime p) (hS : IsUnramifiedOutside K S) : |NumberField.discr K| ≤ ↑(∏ p ∈ S, p ^ (n * Nat.log p n + n - 1))

theorem GeometryOfNumbers.hermite_theorem (A : Type u_1) [Field A] [CharZero A] (n : ℕ) (S : Finset ℕ) : {K : { F : IntermediateField ℚ A // FiniteDimensional ℚ ↥F } | Module.finrank ℚ ↥↑K = n ∧ IsUnramifiedOutside (↥↑K) S}.Finite

theorem GeometryOfNumbers.arakelov_minkowski_bound (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) {f : NumberField.InfinitePlace K → NNReal} (hc : NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)) : ∃ a ∈ ↑I, a ≠ 0 ∧ ∀ (w : NumberField.InfinitePlace K), w a ≤ ↑(f w)