noncomputable def logEmbedding_def (K : Type u_1) [Field K] [NumberField K] : Additive (NumberField.RingOfIntegers K)ˣ →+ NumberField.Units.dirichletUnitTheorem.logSpace K

theorem logEmbedding_ker_eq_torsion (K : Type u_1) [Field K] [NumberField K] : (NumberField.Units.logEmbedding K).ker = Subgroup.toAddSubgroup (NumberField.Units.torsion K)

noncomputable def def_15_3_size (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : ℝ

def def_15_3_L (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : Set K

theorem def_15_3_size_hom (K : Type u_1) [Field K] [NumberField K] (I₁ I₂ : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f₁ f₂ : NumberField.InfinitePlace K → ℝ) : def_15_3_size K (I₁ * I₂) (f₁ * f₂) = def_15_3_size K I₁ f₁ * def_15_3_size K I₂ f₂

theorem def_15_3_kernel_contains_princ (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : (def_15_3_size K (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) x) fun (w : NumberField.InfinitePlace K) => w x) = 1

theorem def_15_3_L_subset_I_c (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : def_15_3_L K I f ⊆ ↑I

noncomputable def def_15_3_I_c_hom (K : Type u_1) [Field K] [NumberField K] : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K × (NumberField.InfinitePlace K → ℝ) →* FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K

theorem lem_15_7_unitLattice_spans_top (K : Type u_1) [Field K] [NumberField K] : Submodule.span ℝ ↑(NumberField.Units.unitLattice K) = ⊤

theorem lem_15_7_unitLattice_discrete (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(NumberField.Units.unitLattice K)

theorem lem_15_7_unitLattice_inter_ball_finite (K : Type u_1) [Field K] [NumberField K] (r : ℝ) : (↑(NumberField.Units.unitLattice K) ∩ Metric.closedBall 0 r).Finite

def arakelovL (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : Set K

theorem def_15_3_L_eq_arakelovL (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : def_15_3_L K I f = arakelovL K I f

theorem lem_15_7_arakelov_L_finite (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : (arakelovL K I f).Finite

theorem cor_15_8_torsion_finite (K : Type u_1) [Field K] [NumberField K] : Finite ↥(NumberField.Units.torsion K)

theorem cor_15_8_kernel_characterization (K : Type u_1) [Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ} : x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1

theorem cor_15_8_logEmbedding_eq_zero_iff (K : Type u_1) [Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ} : (NumberField.Units.logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ NumberField.Units.torsion K

theorem cor_15_8_torsion_subgroup (K : Type u_1) [Field K] : NumberField.Units.torsion K = CommGroup.torsion (NumberField.RingOfIntegers K)ˣ

theorem cor_15_8_torsion_cyclic (K : Type u_1) [Field K] [NumberField K] : IsCyclic ↥(NumberField.Units.torsion K)

theorem prop_15_9_unit_rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℤ ↥(NumberField.Units.unitLattice K) = NumberField.Units.rank K

theorem rank_eq_card_sub_one (K : Type u_1) [Field K] [NumberField K] : NumberField.Units.rank K = Fintype.card (NumberField.InfinitePlace K) - 1

theorem prop_15_9_L_contains_nonzero (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) {f : NumberField.InfinitePlace K → NNReal} (h : NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)) : ∃ a ∈ arakelovL K ↑I fun (w : NumberField.InfinitePlace K) => ↑(f w), a ≠ 0

theorem prop_15_11_fundSystem_lattice_basis (K : Type u_1) [Field K] [NumberField K] (i : Fin (NumberField.Units.rank K)) : (NumberField.Units.logEmbedding K) (Additive.ofMul (NumberField.Units.fundSystem K i)) = ↑((NumberField.Units.basisUnitLattice K) i)

noncomputable def prop_15_11_basisUnitLattice (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Fin (NumberField.Units.rank K)) ℤ ↥(NumberField.Units.unitLattice K)

theorem prop_15_11_closure_fundSystem_sup_torsion_eq_top (K : Type u_1) [Field K] [NumberField K] : Subgroup.closure (Set.range (NumberField.Units.fundSystem K)) ⊔ NumberField.Units.torsion K = ⊤

theorem thm_15_12_dirichlet_unit_theorem (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ∃! ζe : ↥(NumberField.Units.torsion K) × (Fin (NumberField.Units.rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ ζe.2 i

theorem thm_15_12_units_fg (K : Type u_1) [Field K] [NumberField K] : Monoid.FG (NumberField.RingOfIntegers K)ˣ

theorem thm_15_13_number_field_case (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ∃! ζe : ↥(NumberField.Units.torsion K) × (Fin (NumberField.Units.rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ ζe.2 i

def placesAboveInfty (Fq : Type u_2) (F : Type u_3) [Field Fq] [Field F] [Algebra (RatFunc Fq) F] : Set (Valuation F (WithZero (Multiplicative ℤ)))

noncomputable def FunctionField.unitRank (Fq : Type u_2) (F : Type u_3) [Field Fq] [Field F] [Algebra (RatFunc Fq) F] : ℕ

noncomputable def FunctionField.torsionUnits (Fq : Type u_2) (F : Type u_3) [Field Fq] [Field F] [Algebra (Polynomial Fq) F] : Subgroup (↥(ringOfIntegers Fq F))ˣ

theorem thm_15_13_function_field_case (Fq : Type u_2) (F : Type u_3) [Field Fq] [Finite Fq] [Field F] [Algebra (Polynomial Fq) F] [Algebra (RatFunc Fq) F] [IsScalarTower (Polynomial Fq) (RatFunc Fq) F] [FunctionField Fq F] [Algebra.IsSeparable (RatFunc Fq) F] : Nonempty ((↥(FunctionField.ringOfIntegers Fq F))ˣ ≃* ↥(FunctionField.torsionUnits Fq F) × Multiplicative (Fin (FunctionField.unitRank Fq F) → ℤ))

noncomputable def def_15_16_regulator (K : Type u_1) [Field K] [NumberField K] : ℝ

theorem def_15_16_regulator_pos (K : Type u_1) [Field K] [NumberField K] : 0 < NumberField.Units.regulator K

theorem def_15_16_regulator_ne_zero (K : Type u_1) [Field K] [NumberField K] : NumberField.Units.regulator K ≠ 0

noncomputable def def_15_16_regOfFamily (K : Type u_1) [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) : ℝ

theorem def_15_16_regulator_eq_det (K : Type u_1) [Field K] [NumberField K] (w' : NumberField.InfinitePlace K) (e : { w : NumberField.InfinitePlace K // w ≠ w' } ≃ Fin (NumberField.Units.rank K)) : NumberField.Units.regulator K = |(Matrix.of fun (i w : { w : NumberField.InfinitePlace K // w ≠ w' }) => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (e i))))).det|

noncomputable def arakelovDivisor_size (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : ℝ

def arakelovDivisor_L (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : Set K

theorem arakelovDivisor_size_mul (K : Type u_1) [Field K] [NumberField K] (I₁ I₂ : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f₁ f₂ : NumberField.InfinitePlace K → ℝ) : def_15_3_size K (I₁ * I₂) (f₁ * f₂) = def_15_3_size K I₁ f₁ * def_15_3_size K I₂ f₂

theorem arakelovDivisor_principal_size_eq_one (K : Type u_1) [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : (def_15_3_size K (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) x) fun (w : NumberField.InfinitePlace K) => w x) = 1

theorem arakelovDivisor_L_subset (K : Type u_1) [Field K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : def_15_3_L K I f ⊆ ↑I

noncomputable def arakelovDivisor_projection_hom (K : Type u_1) [Field K] [NumberField K] : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K × (NumberField.InfinitePlace K → ℝ) →* FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K

theorem unitLattice_spans_top (K : Type u_1) [Field K] [NumberField K] : Submodule.span ℝ ↑(NumberField.Units.unitLattice K) = ⊤

theorem unitLattice_discreteTopology (K : Type u_1) [Field K] [NumberField K] : DiscreteTopology ↥(NumberField.Units.unitLattice K)

theorem arakelovL_finite (K : Type u_1) [Field K] [NumberField K] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K) (f : NumberField.InfinitePlace K → ℝ) : (arakelovL K I f).Finite

theorem torsion_finite (K : Type u_1) [Field K] [NumberField K] : Finite ↥(NumberField.Units.torsion K)

theorem mem_torsion_iff_forall_infinitePlace_eq_one (K : Type u_1) [Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ} : x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1

theorem logEmbedding_eq_zero_iff_mem_torsion (K : Type u_1) [Field K] [NumberField K] {x : (NumberField.RingOfIntegers K)ˣ} : (NumberField.Units.logEmbedding K) (Additive.ofMul x) = 0 ↔ x ∈ NumberField.Units.torsion K

theorem torsion_eq_commGroup_torsion (K : Type u_1) [Field K] : NumberField.Units.torsion K = CommGroup.torsion (NumberField.RingOfIntegers K)ˣ

theorem torsion_isCyclic (K : Type u_1) [Field K] [NumberField K] : IsCyclic ↥(NumberField.Units.torsion K)

theorem rootsOfUnity_characterization (K : Type u_1) [Field K] [NumberField K] : Finite ↥(NumberField.Units.torsion K) ∧ IsCyclic ↥(NumberField.Units.torsion K) ∧ ∀ (x : (NumberField.RingOfIntegers K)ˣ), x ∈ NumberField.Units.torsion K ↔ ∀ (w : NumberField.InfinitePlace K), w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x) = 1

theorem unitLattice_finrank_eq_rank (K : Type u_1) [Field K] [NumberField K] : Module.finrank ℤ ↥(NumberField.Units.unitLattice K) = NumberField.Units.rank K

theorem arakelovL_exists_ne_zero (K : Type u_1) [Field K] [NumberField K] (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ) {f : NumberField.InfinitePlace K → NNReal} (h : NumberField.mixedEmbedding.minkowskiBound K I < MeasureTheory.volume (NumberField.mixedEmbedding.convexBodyLT K f)) : ∃ a ∈ arakelovL K ↑I fun (w : NumberField.InfinitePlace K) => ↑(f w), a ≠ 0

theorem logEmbedding_fundSystem_eq_basisUnitLattice (K : Type u_1) [Field K] [NumberField K] (i : Fin (NumberField.Units.rank K)) : (NumberField.Units.logEmbedding K) (Additive.ofMul (NumberField.Units.fundSystem K i)) = ↑((NumberField.Units.basisUnitLattice K) i)

noncomputable def basisOfUnitLattice (K : Type u_1) [Field K] [NumberField K] : Module.Basis (Fin (NumberField.Units.rank K)) ℤ ↥(NumberField.Units.unitLattice K)

theorem closure_fundSystem_sup_torsion (K : Type u_1) [Field K] [NumberField K] : Subgroup.closure (Set.range (NumberField.Units.fundSystem K)) ⊔ NumberField.Units.torsion K = ⊤

theorem unit_eq_torsion_mul_fundSystem_pow (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ∃! ζe : ↥(NumberField.Units.torsion K) × (Fin (NumberField.Units.rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ ζe.2 i

theorem units_fg (K : Type u_1) [Field K] [NumberField K] : Monoid.FG (NumberField.RingOfIntegers K)ˣ

theorem numberField_unit_decomposition (K : Type u_1) [Field K] [NumberField K] (x : (NumberField.RingOfIntegers K)ˣ) : ∃! ζe : ↥(NumberField.Units.torsion K) × (Fin (NumberField.Units.rank K) → ℤ), x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ ζe.2 i

noncomputable def regulatorValue (K : Type u_1) [Field K] [NumberField K] : ℝ

theorem regulator_pos_of_numberField (K : Type u_1) [Field K] [NumberField K] : 0 < NumberField.Units.regulator K

theorem regulator_ne_zero_of_numberField (K : Type u_1) [Field K] [NumberField K] : NumberField.Units.regulator K ≠ 0

noncomputable def regulatorOfFamily (K : Type u_1) [Field K] [NumberField K] (u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) : ℝ

theorem regulator_eq_det_of_fundSystem (K : Type u_1) [Field K] [NumberField K] (w' : NumberField.InfinitePlace K) (e : { w : NumberField.InfinitePlace K // w ≠ w' } ≃ Fin (NumberField.Units.rank K)) : NumberField.Units.regulator K = |(Matrix.of fun (i w : { w : NumberField.InfinitePlace K // w ≠ w' }) => ↑(↑w).mult * Real.log (↑w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.fundSystem K (e i))))).det|