theorem algebraMap_valuation_le_one {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) (k : K) (hk : (IsDedekindDomain.HeightOneSpectrum.valuation K v) k ≤ 1) : (IsDedekindDomain.HeightOneSpectrum.valuation L w) ((algebraMap K L) k) ≤ 1

@[implicit_reducible]

noncomputable instance adicCompletionIntegers_algebra_over_base {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : Algebra (NumberField.RingOfIntegers K) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w)

instance adicCompletionIntegers_isScalarTower_base {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : IsScalarTower (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w)

theorem completionEmbedding_finite_mem_integers {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) : (completionEmbedding_finite v w hw) ↑x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w

theorem completionEmbedding_finite_commutes {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) (r : NumberField.RingOfIntegers K) : (completionEmbedding_finite v w hw) ↑((algebraMap (NumberField.RingOfIntegers K) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) r) = ↑((algebraMap (NumberField.RingOfIntegers K) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w)) r)

noncomputable def completionEmbeddingIntegers {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : FinitePlace.LiesAbove w v) : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) →ₐ[NumberField.RingOfIntegers K] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L w)

noncomputable def integralTensorToProduct {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : TensorProduct (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) →ₐ[NumberField.RingOfIntegers K] (ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑ω)

theorem integralTensorToProduct_injective_Mathlib_Gap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Injective ⇑(integralTensorToProduct v)

theorem integralTensorToProduct_surjective_Mathlib_Gap {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Surjective ⇑(integralTensorToProduct v)

theorem integralTensorToProduct_bijective_aux {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Bijective ⇑(integralTensorToProduct v)

theorem integralTensorToProduct_bijective {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Bijective ⇑(integralTensorToProduct v)

theorem integralTensorToProduct_algebraMap_comm {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (r : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) : (integralTensorToProduct v) ((algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (TensorProduct (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))) r) = (algebraMap (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) ((ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑ω))) r

theorem theorem_11_23_part4_integral_iso {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Nonempty (TensorProduct (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ≃ₐ[↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)] (ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑ω))

theorem corollary_11_26_integral {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Nonempty (TensorProduct (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ≃ₐ[↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)] (ω : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑ω))