inductive NumberField.Adeles.Place (K : Type u_1) [Field K] [NumberField K] : Type u_1

• finite {K : Type u_1} [Field K] [NumberField K] : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K) → Place K
• infinite {K : Type u_1} [Field K] [NumberField K] : InfinitePlace K → Place K

@[implicit_reducible]

noncomputable instance NumberField.Adeles.instDecidableEqPlace (K : Type u_1) [Field K] [NumberField K] : DecidableEq (Place K)

theorem NumberField.Adeles.adicCompletion_finite_residueField (K : Type u_2) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : Finite (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

instance NumberField.Adeles.adicCompletion_compactSpace_integer {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : CompactSpace ↥(Valued.integer (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

instance NumberField.Adeles.adicCompletion_properSpace {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : ProperSpace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

theorem NumberField.Adeles.isCompact_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : IsCompact ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

@[reducible, inline]

abbrev NumberField.Adeles.adeleRing {K : Type u_1} [Field K] [NumberField K] : Type u_1

noncomputable def NumberField.Adeles.placeNorm {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : ℝ

theorem NumberField.Adeles.placeNorm_mul {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x y : K) : placeNorm v (x * y) = placeNorm v x * placeNorm v y

theorem NumberField.Adeles.placeNorm_nonneg {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : 0 ≤ placeNorm v x

noncomputable def NumberField.Adeles.placeNormAdele {K : Type u_1} [Field K] [NumberField K] (v : Place K) (a : adeleRing) : ℝ

theorem NumberField.Adeles.placeNorm_eq_placeNormAdele_algebraMap {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) : placeNorm v x = placeNormAdele v ((algebraMap K adeleRing) x)

noncomputable def NumberField.Adeles.adelicAbsVal {K : Type u_1} [Field K] [NumberField K] (a : adeleRing) : ℝ

theorem NumberField.Adeles.restrictedProduct_topology_eq_iSup {ι : Type u_2} (X : ι → Type u_3) (U : (i : ι) → Set (X i)) [(i : ι) → TopologicalSpace (X i)] (𝓕 : Filter ι) : RestrictedProduct.topologicalSpace X U 𝓕 = ⨆ (S : Set ι), ⨆ (hS : 𝓕 ≤ Filter.principal S), TopologicalSpace.coinduced (RestrictedProduct.inclusion X U hS) (RestrictedProduct.topologicalSpace X U (Filter.principal S))

theorem NumberField.Adeles.restrictedProduct_inclusion_isEmbedding {ι : Type u_2} (X : ι → Type u_3) (U : (i : ι) → Set (X i)) [(i : ι) → TopologicalSpace (X i)] {𝓕 : Filter ι} {S : Set ι} (hS : 𝓕 ≤ Filter.principal S) : Topology.IsEmbedding (RestrictedProduct.inclusion X U hS)

theorem NumberField.Adeles.restrictedProduct_inclusion_isOpenEmbedding {ι : Type u_2} (X : ι → Type u_3) (U : (i : ι) → Set (X i)) [(i : ι) → TopologicalSpace (X i)] (hU_open : ∀ (i : ι), IsOpen (U i)) {S : Set ι} (hS : Filter.cofinite ≤ Filter.principal S) : Topology.IsOpenEmbedding (RestrictedProduct.inclusion X U hS)

theorem NumberField.Adeles.restrictedProduct_continuous_iff {ι : Type u_2} (X : ι → Type u_3) (U : (i : ι) → Set (X i)) [(i : ι) → TopologicalSpace (X i)] {𝓕 : Filter ι} {Y : Type u_4} [TopologicalSpace Y] {f : RestrictedProduct (fun (i : ι) => X i) (fun (i : ι) => U i) 𝓕 → Y} : Continuous f ↔ ∀ (S : Set ι) (hS : 𝓕 ≤ Filter.principal S), Continuous (f ∘ RestrictedProduct.inclusion X U hS)

theorem NumberField.Adeles.finiteAdeleRing_topology_eq_iSup {K : Type u_1} [Field K] [NumberField K] : RestrictedProduct.topologicalSpace (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) Filter.cofinite = ⨆ (S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))), ⨆ (hS : Filter.cofinite ≤ Filter.principal S), TopologicalSpace.coinduced (RestrictedProduct.inclusion (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) hS) (RestrictedProduct.topologicalSpace (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (Filter.principal S))

theorem NumberField.Adeles.finiteAdeleRing_inclusion_isOpenEmbedding {K : Type u_1} [Field K] [NumberField K] {S : Set (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))} (hS : Filter.cofinite ≤ Filter.principal S) : Topology.IsOpenEmbedding (RestrictedProduct.inclusion (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) hS)

instance NumberField.Adeles.adeleRing_isTopologicalRing {K : Type u_1} [Field K] [NumberField K] : IsTopologicalRing adeleRing

instance NumberField.Adeles.infiniteAdeleRing_t2Space {K : Type u_1} [Field K] : T2Space (InfiniteAdeleRing K)

instance NumberField.Adeles.finiteAdeleRing_t2Space {K : Type u_1} [Field K] [NumberField K] : T2Space (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)

instance NumberField.Adeles.adeleRing_t2Space {K : Type u_1} [Field K] [NumberField K] : T2Space adeleRing

instance NumberField.Adeles.finiteAdeleRing_locallyCompactSpace {K : Type u_1} [Field K] [NumberField K] : LocallyCompactSpace (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)

instance NumberField.Adeles.adeleRing_locallyCompactSpace {K : Type u_1} [Field K] [NumberField K] : LocallyCompactSpace adeleRing

theorem NumberField.Adeles.diag_injective {K : Type u_1} [Field K] [NumberField K] : Function.Injective ⇑(algebraMap K adeleRing)

@[reducible, inline]

noncomputable abbrev NumberField.Adeles.principalSubgroup {K : Type u_1} [Field K] [NumberField K] : AddSubgroup adeleRing

theorem NumberField.Adeles.eq_zero_of_integral_and_inf_lt_one {K : Type u_1} [Field K] [NumberField K] (k : RingOfIntegers K) (hinf : ∀ (w : InfinitePlace K), w ((algebraMap (RingOfIntegers K) K) k) < 1) : k = 0

theorem NumberField.Adeles.mem_ringOfIntegers_of_finiteAdele_integral {K : Type u_1} [Field K] [NumberField K] (x : K) (h : (algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x ∈ Set.range (RestrictedProduct.structureMap (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) Filter.cofinite)) : x ∈ (algebraMap (RingOfIntegers K) K).range

theorem NumberField.Adeles.principalAdeles_discrete {K : Type u_1} [Field K] [NumberField K] : DiscreteTopology ↥principalSubgroup

instance NumberField.Adeles.infinitePlace_properSpace {K : Type u_1} [Field K] (v : InfinitePlace K) : ProperSpace v.Completion

theorem NumberField.Adeles.isCompact_finiteAdeleRing_integralSet {K : Type u_1} [Field K] [NumberField K] : IsCompact {a : IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K | ∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), a v ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)}

theorem NumberField.Adeles.adeles_integral_set_compact {K : Type u_1} [Field K] [NumberField K] : IsCompact ((Set.univ.pi fun (v : InfinitePlace K) => Metric.closedBall 0 1) ×ˢ {a : IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K | ∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), a v ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)})

theorem NumberField.Adeles.valued_algebraMap_eq_valuation_crt {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : Valued.v ((algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x) = (IsDedekindDomain.HeightOneSpectrum.valuation K v) x

theorem NumberField.Adeles.algebraMap_div_mem_adicCompletionIntegers_crt {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (r d : RingOfIntegers K) (h : v.intValuation r ≤ v.intValuation d) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (↑r / ↑d) ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.Adeles.intValuation_le_exp_of_mem_pow_crt {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (r : RingOfIntegers K) (n : ℕ) (hr : r ∈ v.asIdeal ^ n) : v.intValuation r ≤ WithZero.exp (-↑n)

theorem NumberField.Adeles.intValuation_le_of_mem_pow_ge_crt {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (r d : RingOfIntegers K) (hd : d ≠ 0) (n : ℕ) (hn : (-(v.intValuation d).log).toNat ≤ n) (hr : r ∈ v.asIdeal ^ n) : v.intValuation r ≤ v.intValuation d

theorem NumberField.Adeles.exists_integral_approx_at_place {K : Type u_2} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : ∃ (c : K), x - (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) c ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.Adeles.crt_finite_places_covering (K : Type u_2) [Field K] [NumberField K] (a : IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) : ∃ (c : K), ∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), a v - (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) c ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

noncomputable def NumberField.Adeles.coveringBound (K : Type u_2) [Field K] [NumberField K] : ℝ

theorem NumberField.Adeles.one_le_coveringBound (K : Type u_2) [Field K] [NumberField K] : 1 ≤ coveringBound K

theorem NumberField.Adeles.coveringBound_pos (K : Type u_2) [Field K] [NumberField K] : 0 < coveringBound K

theorem NumberField.Adeles.coveringBound_ne_zero (K : Type u_2) [Field K] [NumberField K] : coveringBound K ≠ 0

theorem NumberField.Adeles.coveringBound_nonneg (K : Type u_2) [Field K] [NumberField K] : 0 ≤ coveringBound K

theorem NumberField.Adeles.lattice_covering_infinite_places (K : Type u_2) [Field K] [NumberField K] (f : InfiniteAdeleRing K) (c₁ : K) : ∃ (r : RingOfIntegers K), ∀ (w : InfinitePlace K), ‖f w - (algebraMap K w.Completion) (c₁ + (algebraMap (RingOfIntegers K) K) r)‖ ≤ coveringBound K

theorem NumberField.Adeles.crt_covering {K : Type u_1} [Field K] [NumberField K] (a : adeleRing) : ∃ (c : K), (∀ (w : InfinitePlace K), ‖a.1 w - (algebraMap K w.Completion) c‖ ≤ coveringBound K) ∧ ∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), a.2 v - (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) c ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.Adeles.adeles_compact_fundamental_domain {K : Type u_1} [Field K] [NumberField K] : ∃ (W : Set adeleRing), IsCompact W ∧ ∀ (a : adeleRing), ∃ (c : K), a - (algebraMap K adeleRing) c ∈ W

theorem NumberField.Adeles.principalAdeles_cocompact {K : Type u_1} [Field K] [NumberField K] : CompactSpace (adeleRing ⧸ principalSubgroup)

def NumberField.Adeles.PiTensorCompletion (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [Algebra K L] : Type (max u_2 u_3)

@[implicit_reducible]

noncomputable instance NumberField.Adeles.piTensorCompletion_commRing (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [Algebra K L] : CommRing (PiTensorCompletion K L)

noncomputable def NumberField.Adeles.tensorCompletionToFiberProd (K : Type u_2) (L : Type u_3) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : InfinitePlace K) : TensorProduct K L v.Completion →+* (w : { w : InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion

theorem NumberField.Adeles.tensorCompletionToFiberProd_bijective (K : Type u_2) (L : Type u_3) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : InfinitePlace K) : Function.Bijective ⇑(tensorCompletionToFiberProd K L v)

theorem NumberField.Adeles.infinitePlace_baseChange_decomposition (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (v : InfinitePlace K) : ∃ (e : TensorProduct K L v.Completion ≃+* ((w : { w : InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion)), ∀ (l : L), e (l ⊗ₜ[K] 1) = fun (w : { w : InfinitePlace L // w.comap (algebraMap K L) = v }) => (algebraMap L (↑w).Completion) l

def NumberField.Adeles.sigmaPiRegroup (K : Type u_2) (L : Type u_3) [Field K] [Field L] [Algebra K L] : ((v : InfinitePlace K) → (w : { w : InfinitePlace L // w.comap (algebraMap K L) = v }) → (↑w).Completion) ≃+* InfiniteAdeleRing L

theorem NumberField.Adeles.completion_tensor_pi_equiv (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : PiTensorCompletion K L ≃+* InfiniteAdeleRing L), ∀ (l : L), (e fun (v : InfinitePlace K) => l ⊗ₜ[K] 1) = (algebraMap L (InfiniteAdeleRing L)) l

theorem NumberField.Adeles.infiniteAdeleRing_base_change_iso (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Nonempty (TensorProduct K (InfiniteAdeleRing K) L ≃+* InfiniteAdeleRing L)

@[implicit_reducible]

noncomputable instance NumberField.Adeles.finAdeleRing_algebra_base (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Algebra K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)

instance NumberField.Adeles.finAdeleRing_scalarTower_base_base (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : IsScalarTower K K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)

instance NumberField.Adeles.finAdeleRing_scalarTower_base_ext (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : IsScalarTower K L (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)

noncomputable def NumberField.Adeles.primeBelow (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)

noncomputable def NumberField.Adeles.localBaseChangeMap (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) : WithVal (IsDedekindDomain.HeightOneSpectrum.valuation K (primeBelow K L w)) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion L w

theorem NumberField.Adeles.localBaseChangeMap_continuous (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) : Continuous ⇑(localBaseChangeMap K L w)

noncomputable def NumberField.Adeles.baseChangeAtPrime (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) : IsDedekindDomain.HeightOneSpectrum.adicCompletion K (primeBelow K L w) →+* IsDedekindDomain.HeightOneSpectrum.adicCompletion L w

theorem NumberField.Adeles.baseChangeAtPrime_mem_integers (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K (primeBelow K L w)) (hx : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K (primeBelow K L w)) : (baseChangeAtPrime K L w) x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w

theorem NumberField.Adeles.baseChange_restricted_condition (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (a : IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) : ∀ᶠ (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) in Filter.cofinite, (baseChangeAtPrime K L w) (a (primeBelow K L w)) ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w

theorem NumberField.Adeles.baseChange_commutes (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (k : K) : RestrictedProduct.mk (fun (w : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers L)) => (baseChangeAtPrime K L w) (((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) k) (primeBelow K L w))) ⋯ = (algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)) k

noncomputable def NumberField.Adeles.finAdeleRing_baseChangeHom (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K →ₐ[K] IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L

noncomputable def NumberField.Adeles.finAdeleRing_includeExt (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : L →ₐ[K] IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L

noncomputable def NumberField.Adeles.finAdeleRing_tensor_forward (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L →ₐ[K] IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L

theorem NumberField.Adeles.finAdeleRing_tensor_forward_isAlgEquiv (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃ₐ[K] IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L), ↑e = finAdeleRing_tensor_forward K L

theorem NumberField.Adeles.finAdeleRing_tensor_forward_toRingHom_bijective (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Function.Bijective ⇑(finAdeleRing_tensor_forward K L).toRingHom

theorem NumberField.Adeles.finAdeleRing_tensor_equiv_of_referenced_results (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃+* IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L), e.toRingHom = (finAdeleRing_tensor_forward K L).toRingHom

theorem NumberField.Adeles.finAdeleRing_tensor_forward_bijective (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Function.Bijective ⇑(finAdeleRing_tensor_forward K L).toRingHom

noncomputable def NumberField.Adeles.finiteAdeleRing_tensor_ringEquiv (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃+* IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L

theorem NumberField.Adeles.finiteAdeleRing_tensor_ringEquiv_compat (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (l : L) : (finiteAdeleRing_tensor_ringEquiv K L) (Algebra.TensorProduct.includeRight l) = (algebraMap L (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)) l

theorem NumberField.Adeles.finiteAdeleRing_tensor_equiv (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃+* IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L), ∀ (l : L), e (Algebra.TensorProduct.includeRight l) = (algebraMap L (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)) l

theorem NumberField.Adeles.finiteAdeleRing_base_change_iso (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Nonempty (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃+* IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)

theorem NumberField.Adeles.adeles_base_change {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : Nonempty (AdeleRing (RingOfIntegers L) L ≃+* TensorProduct K (AdeleRing (RingOfIntegers K) K) L)

theorem NumberField.Adeles.infiniteAdeleRing_base_change_diagram_aux (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : TensorProduct K (InfiniteAdeleRing K) L ≃+* InfiniteAdeleRing L), ∀ (l : L), e (Algebra.TensorProduct.includeRight l) = (algebraMap L (InfiniteAdeleRing L)) l

theorem NumberField.Adeles.finiteAdeleRing_base_change_diagram_aux (K : Type u_2) (L : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (e : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K) L ≃+* IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L), ∀ (l : L), e (Algebra.TensorProduct.includeRight l) = (algebraMap L (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers L) L)) l

theorem NumberField.Adeles.adeles_base_change_diagram {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : ∃ (φ : AdeleRing (RingOfIntegers L) L ≃+* TensorProduct K (AdeleRing (RingOfIntegers K) K) L), ∀ (l : L), φ ((algebraMap L (AdeleRing (RingOfIntegers L) L)) l) = Algebra.TensorProduct.includeRight.toRingHom l

@[implicit_reducible]

noncomputable instance NumberField.Adeles.adeleRing_algebra_base {K : Type u_1} [Field K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] : Algebra K (AdeleRing (RingOfIntegers L) L)

theorem NumberField.Adeles.adeleRing_algebra_base_algebraMap {K : Type u_1} [Field K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] : algebraMap K (AdeleRing (RingOfIntegers L) L) = (algebraMap L (AdeleRing (RingOfIntegers L) L)).comp (algebraMap K L)

theorem NumberField.Adeles.adeles_baseChange_continuous_fwd {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] (φ : AdeleRing (RingOfIntegers L) L ≃+* TensorProduct K (AdeleRing (RingOfIntegers K) K) L) (b : Module.Basis (Fin (Module.finrank K L)) K L) : Continuous fun (x : AdeleRing (RingOfIntegers L) L) => (Algebra.TensorProduct.equivPiOfFiniteBasis (AdeleRing (RingOfIntegers K) K) b) (φ x)

theorem NumberField.Adeles.adeles_baseChange_continuous_inv {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : let x := Algebra.toModule; ∀ (φ : AdeleRing (RingOfIntegers L) L ≃+* TensorProduct K (AdeleRing (RingOfIntegers K) K) L) (b : Module.Basis (Fin (Module.finrank K L)) K L), Continuous fun (y : Fin (Module.finrank K L) → AdeleRing (RingOfIntegers K) K) => φ.symm ((Algebra.TensorProduct.equivPiOfFiniteBasis (AdeleRing (RingOfIntegers K) K) b).symm y)

noncomputable def NumberField.Adeles.adeleRing_directSumDecomposition {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : AdeleRing (RingOfIntegers L) L ≃L[K] Fin (Module.finrank K L) → AdeleRing (RingOfIntegers K) K

theorem NumberField.Adeles.adeleRing_directSumDecomposition_principalRestriction {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] [FiniteDimensional K L] : have φ := adeleRing_directSumDecomposition L; have b := Module.finBasis K L; ∀ (l : L), φ ((algebraMap L (AdeleRing (RingOfIntegers L) L)) l) = fun (i : Fin (Module.finrank K L)) => (algebraMap K (AdeleRing (RingOfIntegers K) K)) (b.equivFun l i)

def NumberField.Adeles.adelicBox {K : Type u_1} [Field K] [NumberField K] (a : adeleRing) : Set adeleRing

theorem NumberField.Adeles.haar_blichfeldt_pigeonhole_axiom (K : Type u_2) [Field K] [NumberField K] (a : adeleRing) (ha : adelicAbsVal a > 0) : ∃ (s₁ : adeleRing) (s₂ : adeleRing), s₁ ∈ adelicBox a ∧ s₂ ∈ adelicBox a ∧ s₁ ≠ s₂ ∧ s₁ - s₂ ∈ ↑principalSubgroup

theorem NumberField.Adeles.adeleRing_adelicBox_blichfeldt (K : Type u_2) [Field K] [NumberField K] (a : adeleRing) (ha : adelicAbsVal a > 0) : ∃ (s₁ : adeleRing) (s₂ : adeleRing), s₁ ∈ adelicBox a ∧ s₂ ∈ adelicBox a ∧ s₁ ≠ s₂ ∧ ∃ (c : K), s₁ - s₂ = (algebraMap K adeleRing) c

theorem NumberField.Adeles.adelicBox_blichfeldt_pigeonhole (K : Type u_2) [Field K] [NumberField K] (b₀ b₁ : ℝ) (hb₀ : 0 < b₀) (hb₁ : 0 < b₁) (a : adeleRing) (ha : b₁ * adelicAbsVal a > b₀) : ∃ (s₁ : adeleRing) (s₂ : adeleRing), s₁ ∈ adelicBox a ∧ s₂ ∈ adelicBox a ∧ s₁ ≠ s₂ ∧ ∃ (c : K), s₁ - s₂ = (algebraMap K adeleRing) c

theorem NumberField.Adeles.adelic_blichfeldt_pigeonhole_aux (K : Type u_2) [Field K] [NumberField K] : ∃ (b₀ : ℝ) (b₁ : ℝ), 0 < b₀ ∧ 0 < b₁ ∧ ∀ (a : adeleRing), b₁ * adelicAbsVal a > b₀ → ∃ (s₁ : adeleRing) (s₂ : adeleRing), s₁ ∈ adelicBox a ∧ s₂ ∈ adelicBox a ∧ s₁ ≠ s₂ ∧ ∃ (c : K), s₁ - s₂ = (algebraMap K adeleRing) c

theorem NumberField.Adeles.exists_pair_in_box_with_nonzero_diff (K : Type u_2) [Field K] [NumberField K] : ∃ (b₀ : ℝ) (b₁ : ℝ), 0 < b₀ ∧ 0 < b₁ ∧ ∀ (a : adeleRing), b₁ * adelicAbsVal a > b₀ → ∃ (s₁ : adeleRing) (s₂ : adeleRing) (c : K), s₁ ∈ adelicBox a ∧ s₂ ∈ adelicBox a ∧ c ≠ 0 ∧ s₁ - s₂ = (algebraMap K adeleRing) c

theorem NumberField.Adeles.haar_blichfeldt_constants (K : Type u_2) [Field K] [NumberField K] : ∃ (b₀ : ℝ) (b₁ : ℝ), 0 < b₀ ∧ 0 < b₁ ∧ ∀ (a : adeleRing), b₁ * adelicAbsVal a > b₀ → ∃ (x : K) (y : K), x ≠ y ∧ ((fun (s : adeleRing) => (algebraMap K adeleRing) x + s) '' adelicBox a ∩ (fun (s : adeleRing) => (algebraMap K adeleRing) y + s) '' adelicBox a).Nonempty

theorem NumberField.Adeles.adelic_box_translates_overlap (K : Type u_2) [Field K] [NumberField K] : ∃ (B : ℝ), 0 < B ∧ ∀ (a : adeleRing), adelicAbsVal a > B → ∃ (x : K) (y : K), x ≠ y ∧ ((fun (s : adeleRing) => (algebraMap K adeleRing) x + s) '' adelicBox a ∩ (fun (s : adeleRing) => (algebraMap K adeleRing) y + s) '' adelicBox a).Nonempty

theorem NumberField.Adeles.adelic_blichfeldt_for_box {K : Type u_1} [Field K] [NumberField K] : ∃ (B : ℝ), 0 < B ∧ ∀ (a : adeleRing), adelicAbsVal a > B → ∃ t₁ ∈ adelicBox a, ∃ t₂ ∈ adelicBox a, t₁ ≠ t₂ ∧ t₁ - t₂ ∈ Set.range ⇑(algebraMap K adeleRing)

theorem NumberField.Adeles.adelic_pigeonhole_haar {K : Type u_1} [Field K] [NumberField K] : ∃ (B : ℝ), 0 < B ∧ ∀ (a : adeleRing), adelicAbsVal a > B → ∃ (t₁ : adeleRing) (t₂ : adeleRing), t₁ ≠ t₂ ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), ‖t₁.2 v‖ ≤ ‖a.2 v‖) ∧ (∀ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), ‖t₂.2 v‖ ≤ ‖a.2 v‖) ∧ (∀ (w : InfinitePlace K), ‖t₁.1 w‖ ≤ ‖a.1 w‖ / 4) ∧ (∀ (w : InfinitePlace K), ‖t₂.1 w‖ ≤ ‖a.1 w‖ / 4) ∧ t₁ - t₂ ∈ Set.range ⇑(algebraMap K adeleRing)

theorem NumberField.Adeles.adelic_blichfeldt_minkowski {K : Type u_1} [Field K] [NumberField K] : ∃ (B : ℝ), 0 < B ∧ ∀ (a : adeleRing), adelicAbsVal a > B → ∃ (x : K), x ≠ 0 ∧ ∀ (v : Place K), placeNormAdele v ((algebraMap K adeleRing) x) ≤ placeNormAdele v a

instance NumberField.Adeles.instNormOneClass_Completion {K : Type u_1} [Field K] (w : InfinitePlace K) : NormOneClass w.Completion

@[implicit_reducible]

noncomputable instance NumberField.Adeles.instNontrivNormedField_InfCompl {K : Type u_1} [Field K] (w : InfinitePlace K) : NontriviallyNormedField w.Completion

theorem NumberField.Adeles.mem_adicCompletionIntegers_iff_norm_le_one {K : Type u_1} [Field K] [NumberField K] (vi : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K vi) : x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K vi ↔ ‖x‖ ≤ 1

theorem NumberField.Adeles.exists_strategic_adele {K : Type u_1} [Field K] [NumberField K] (B : ℝ) (hB : 0 < B) (S : Finset (Place K)) (w : Place K) (hw : w ∉ S) (ε : (v : Place K) → v ∈ S → ℝ) (hε : ∀ (v : Place K) (hv : v ∈ S), 0 < ε v hv) : ∃ (z : adeleRing), adelicAbsVal z > B ∧ (∀ (v : Place K) (hv : v ∈ S), placeNormAdele v z ≤ ε v hv) ∧ (∀ v ∉ S, v ≠ w → placeNormAdele v z ≤ 1) ∧ (Function.mulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) => ‖z.2 v‖).Finite

theorem NumberField.Adeles.exists_element_with_controlled_norms {K : Type u_1} [Field K] [NumberField K] (S : Finset (Place K)) (w : Place K) (hw : w ∉ S) (ε : (v : Place K) → v ∈ S → ℝ) (hε : ∀ (v : Place K) (hv : v ∈ S), 0 < ε v hv) : ∃ (u : K), u ≠ 0 ∧ (∀ (v : Place K) (hv : v ∈ S), placeNorm v u ≤ ε v hv) ∧ ∀ v ∉ S, v ≠ w → placeNorm v u ≤ 1

theorem NumberField.Adeles.adicAbv_le_one_of_mem_integers_algebraMap {K : Type u_1} [Field K] [NumberField K] (vi : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) (hx : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K vi)) x ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K vi)) : (HeightOneSpectrum.adicAbv K vi) x ≤ 1

theorem NumberField.Adeles.placeNorm_infinite_eq_norm_algebraMap {K : Type u_1} [Field K] (w : InfinitePlace K) (x : K) : w x = ‖(algebraMap K w.Completion) x‖

theorem NumberField.Adeles.adeles_K_plus_unit_ball {K : Type u_1} [Field K] [NumberField K] (S : Finset (Place K)) (a : (v : Place K) → v ∈ S → K) : ∃ (c : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (c - a v hv) ≤ coveringBound K) ∧ ∀ v ∉ S, placeNorm v c ≤ coveringBound K

theorem NumberField.Adeles.adelic_scaling_decomposition {K : Type u_1} [Field K] [NumberField K] (u : K) (hu : u ≠ 0) (S : Finset (Place K)) (a : (v : Place K) → v ∈ S → K) : ∃ (x : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (x - a v hv) ≤ placeNorm v u * coveringBound K) ∧ ∀ v ∉ S, placeNorm v x ≤ placeNorm v u * coveringBound K

theorem NumberField.Adeles.strong_approximation {K : Type u_1} [Field K] [NumberField K] (S : Finset (Place K)) (w : Place K) (hw : w ∉ S) (a : (v : Place K) → v ∈ S → K) (ε : (v : Place K) → v ∈ S → ℝ) (hε : ∀ (v : Place K) (hv : v ∈ S), 0 < ε v hv) : ∃ (x : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (x - a v hv) ≤ ε v hv) ∧ ∀ v ∉ S, v ≠ w → placeNorm v x ≤ 1

theorem NumberField.Adeles.global_field_dense_awayFrom {K : Type u_1} [Field K] [NumberField K] (w : Place K) (S : Finset (Place K)) (hw : w ∉ S) (a : (v : Place K) → v ∈ S → K) (ε : ℝ) (hε : 0 < ε) : ∃ (x : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (x - a v hv) ≤ ε) ∧ ∀ v ∉ S, v ≠ w → placeNorm v x ≤ 1

theorem NumberField.Adeles.placeNorm_finite_le_one_imp_mem_integers {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) (hx : placeNorm (Place.finite v) x ≤ 1) : ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.Adeles.algebraMap_finiteAdeleRing_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v = (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) x

theorem NumberField.Adeles.norm_algebraMap_finiteAdeleRing_eq {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x : K) : ‖((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v‖ = placeNorm (Place.finite v) x

theorem NumberField.Adeles.strong_approx_integral_to_mem_integers {K : Type u_1} [Field K] [NumberField K] (x : K) (S : Finset (IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K))) (hx : ∀ v ∉ S, placeNorm (Place.finite v) x ≤ 1) (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : v ∉ S → ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v ∈ ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.Adeles.norm_algebraMap_finiteAdeleRing_sub {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x y : K) : ‖((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v - ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) y) v‖ = placeNorm (Place.finite v) (x - y)

theorem NumberField.Adeles.algebraMap_finiteAdeleRing_sub_apply {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) (x y : K) : ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) (x - y)) v = ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x) v - ((algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) y) v

theorem NumberField.Adeles.adeles_K_plus_unit_ball_finite_le_one {K : Type u_1} [Field K] [NumberField K] (S : Finset (Place K)) (a : (v : Place K) → v ∈ S → K) : ∃ (c : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (c - a v hv) ≤ coveringBound K) ∧ (∀ v ∉ S, placeNorm v c ≤ coveringBound K) ∧ ∀ (vi : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), Place.finite vi ∉ S → placeNorm (Place.finite vi) c ≤ 1

theorem NumberField.Adeles.adelic_scaling_decomposition_finite_le_one {K : Type u_1} [Field K] [NumberField K] (u : K) (hu : u ≠ 0) (S : Finset (Place K)) (a : (v : Place K) → v ∈ S → K) : ∃ (x : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (x - a v hv) ≤ placeNorm v u * coveringBound K) ∧ (∀ v ∉ S, placeNorm v x ≤ placeNorm v u * coveringBound K) ∧ ∀ (vi : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), Place.finite vi ∉ S → placeNorm (Place.finite vi) x ≤ placeNorm (Place.finite vi) u * 1

theorem NumberField.Adeles.strong_approximation_finite_le_one {K : Type u_1} [Field K] [NumberField K] (S : Finset (Place K)) (w : Place K) (hw : w ∉ S) (a : (v : Place K) → v ∈ S → K) (ε : (v : Place K) → v ∈ S → ℝ) (hε : ∀ (v : Place K) (hv : v ∈ S), 0 < ε v hv) : ∃ (x : K), (∀ (v : Place K) (hv : v ∈ S), placeNorm v (x - a v hv) ≤ ε v hv) ∧ (∀ v ∉ S, v ≠ w → placeNorm v x ≤ 1) ∧ ∀ (vi : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), Place.finite vi ∉ S → Place.finite vi ≠ w → placeNorm (Place.finite vi) x ≤ 1

theorem NumberField.Adeles.denseRange_algebraMap_finiteAdeleRing {K : Type u_1} [Field K] [NumberField K] : DenseRange ⇑(algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K))

theorem NumberField.Adeles.global_field_dense_in_infiniteAdeleRing {K : Type u_1} [Field K] [NumberField K] : Dense (Set.range ⇑(algebraMap K (InfiniteAdeleRing K)))

theorem NumberField.Adeles.denseRange_algebraMap_adeleRing_components {K : Type u_1} [Field K] [NumberField K] : DenseRange ⇑(algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) ∧ DenseRange ⇑(algebraMap K (InfiniteAdeleRing K))

@[reducible]

def NumberField.Adeles.placeCompletion {K : Type u_1} [Field K] [NumberField K] : Place K → Type u_1

@[implicit_reducible]

noncomputable instance NumberField.Adeles.instTopologicalSpacePlaceCompletion {K : Type u_1} [Field K] [NumberField K] (v : Place K) : TopologicalSpace (placeCompletion v)

def NumberField.Adeles.placeIntegerSet {K : Type u_1} [Field K] [NumberField K] (v : Place K) : Set (placeCompletion v)

@[reducible, inline]

abbrev NumberField.Adeles.restrictedProductAwayFrom {K : Type u_1} [Field K] [NumberField K] (w : Place K) : Type u_1

@[reducible]

noncomputable def NumberField.Adeles.embedAtPlace {K : Type u_1} [Field K] [NumberField K] (v : Place K) : K → placeCompletion v

noncomputable def NumberField.Adeles.diagonalAwayFrom {K : Type u_1} [Field K] [NumberField K] (w : Place K) (x : K) : restrictedProductAwayFrom w

theorem NumberField.Adeles.isOpen_placeIntegerSet {K : Type u_1} [Field K] [NumberField K] (v : Place K) : IsOpen (placeIntegerSet v)

theorem NumberField.Adeles.placeNorm_le_one_imp_mem_placeIntegerSet {K : Type u_1} [Field K] [NumberField K] (v : Place K) (x : K) (hx : placeNorm v x ≤ 1) : embedAtPlace v x ∈ placeIntegerSet v

theorem NumberField.Adeles.infPlace_norm_algebraMap {K : Type u_1} [Field K] (wi : InfinitePlace K) (x : K) : ‖(algebraMap K wi.Completion) x‖ = ↑wi x

theorem NumberField.Adeles.infPlace_denseRange_algebraMap {K : Type u_1} [Field K] (wi : InfinitePlace K) : DenseRange ⇑(algebraMap K wi.Completion)

theorem NumberField.Adeles.dense_diagonalAwayFrom {K : Type u_1} [Field K] [NumberField K] (w : Place K) : Dense (Set.range (diagonalAwayFrom w))