theorem finrank_le_two_of_isReal_place {K : Type} [Field K] [NumberField K] {v : NumberField.InfinitePlace K} (hv : v.IsReal) (M : Type u_1) [Field M] [Algebra v.Completion M] [FiniteDimensional v.Completion M] : Module.finrank v.Completion M ≤ 2

theorem exists_degree_two_extension_above_real_place {K : Type} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) (hv : v.IsReal) (M : Type u_1) [Field M] [Algebra v.Completion M] [FiniteDimensional v.Completion M] [Algebra.IsSeparable v.Completion M] (hfin : Module.finrank v.Completion M = 2) : ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K L) = v), Module.finrank K L = 2 ∧ ∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)

theorem finrank_eq_one_of_isAlgClosed (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [IsAlgClosed F] [FiniteDimensional F E] : Module.finrank F E = 1

noncomputable def algEquivOfFinrankOne (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (h : Module.finrank F E = 1) : E ≃ₐ[F] F

theorem exists_heightOneSpectrum_above {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)), Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal

theorem exists_monic_approx_poly {K : Type u_1} [Field K] {K_v : Type u_2} [NontriviallyNormedField K_v] [Algebra K K_v] (hdense : DenseRange ⇑(algebraMap K K_v)) (f : Polynomial K_v) (hf_monic : f.Monic) (hf_deg : 0 < f.natDegree) (δ : ℝ) (hδ : 0 < δ) : ∃ (g : Polynomial K), g.Monic ∧ g.natDegree = f.natDegree ∧ Polynomial.L1norm (normAbsVal K_v) (f - Polynomial.map (algebraMap K K_v) g) < δ

theorem krasner_irreducible {K_v : Type u_1} [NontriviallyNormedField K_v] [IsUltrametricDist K_v] [CompleteSpace K_v] (f g : Polynomial K_v) (hf_monic : f.Monic) (hf_irr : Irreducible f) (hf_sep : f.Separable) (hg_monic : g.Monic) (hg_deg : g.natDegree = f.natDegree) (hclose : ∃ (δ : ℝ), 0 < δ ∧ Polynomial.L1norm (normAbsVal K_v) (f - g) < δ ∧ ∀ (g' : Polynomial K_v), g'.Monic → g'.natDegree = f.natDegree → Polynomial.L1norm (normAbsVal K_v) (f - g') < δ → ∀ (β : AlgebraicClosure K_v), (Polynomial.aeval β) g' = 0 → ∃ (α : AlgebraicClosure K_v), (Polynomial.aeval α) f = 0 ∧ K_v⟮α⟯ = K_v⟮β⟯) : Irreducible g

theorem algEquiv_adjoinRoot_of_root (F : Type u_1) [Field F] (g : Polynomial F) (hg_irr : Irreducible g) (hg_monic : g.Monic) (M : Type u_2) [Field M] [Algebra F M] [FiniteDimensional F M] (hM_deg : Module.finrank F M = g.natDegree) (α : M) (hα : (Polynomial.aeval α) g = 0) : Nonempty (M ≃ₐ[F] AdjoinRoot g)

theorem adjoinRoot_equiv_of_intermediateField_eq (K : Type u_1) [Field K] (E : Type u_2) [Field E] [Algebra K E] (p q : Polynomial K) (hp_irr : Irreducible p) (hp_monic : p.Monic) (hq_irr : Irreducible q) (hq_monic : q.Monic) (α β : E) (hα : (Polynomial.aeval α) p = 0) (hβ : (Polynomial.aeval β) q = 0) (heq : K⟮α⟯ = K⟮β⟯) : Nonempty (AdjoinRoot p ≃ₐ[K] AdjoinRoot q)

theorem adicCompletion_finiteDimensional_of_adjoinRoot {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (L : Type) [Field L] [NumberField L] [Algebra K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] (hL_eq : L = AdjoinRoot g) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal) (instAlg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) : FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

theorem adicCompletion_finrank_eq_natDegree {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (L : Type) [Field L] [NumberField L] [Algebra K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] (hL_eq : L = AdjoinRoot g) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal) (instAlg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) : Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) = g.natDegree

theorem adicCompletion_root_exists {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (L : Type) [Field L] [NumberField L] [Algebra K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] (hL_eq : L = AdjoinRoot g) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal) (instAlg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) : ∃ (x : IsDedekindDomain.HeightOneSpectrum.adicCompletion L w), (Polynomial.aeval x) (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g) = 0

theorem adicCompletion_algEquiv_adjoinRoot_of_adjoinRoot {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (L : Type) [Field L] [NumberField L] [Algebra K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] (hL_eq : L = AdjoinRoot g) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal) (instAlg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] AdjoinRoot (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g))

theorem adicCompletion_algEquiv_of_adjoinRoot {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] (hM_deg : Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M = g.natDegree) (L : Type) [Field L] [NumberField L] [Algebra K L] [Algebra.IsSeparable K L] [FiniteDimensional K L] (hL_eq : L = AdjoinRoot g) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (hw : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal) (instAlg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) (hM_equiv : Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] AdjoinRoot (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g))) : Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

theorem adjoinRoot_adicCompletion_exists {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (g : Polynomial K) (hg_irr : Irreducible g) (hg_monic : g.Monic) (hg_map_irr : Irreducible (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] (hM_deg : Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M = g.natDegree) (hM_equiv : Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] AdjoinRoot (Polynomial.map (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) g))) : ∃ (L : Type) (x : Field L) (x_1 : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (_ : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal), Module.finrank K L = g.natDegree ∧ ∃ (x_6 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

theorem separableExtension_isCompletion_finitePlace {K : Type} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] : ∃ (L : Type) (x : Field L) (x_1 : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (_ : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal), Module.finrank K L = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M ∧ ∃ (x_6 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)

theorem separableExtension_isCompletion_infinitePlace {K : Type} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) (M : Type u_1) [Field M] [Algebra v.Completion M] [FiniteDimensional v.Completion M] [Algebra.IsSeparable v.Completion M] : ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K L) = v), Module.finrank K L = Module.finrank v.Completion M ∧ ∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)

theorem separableExtension_isCompletion {K : Type} [Field K] [NumberField K] : (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (M : Type u_1) [inst : Field M] [inst_1 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M], ∃ (L : Type) (x : Field L) (x_1 : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (_ : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal), Module.finrank K L = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M ∧ ∃ (x_6 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) ∧ ∀ (v : NumberField.InfinitePlace K) (M : Type u_2) [inst : Field M] [inst_1 : Algebra v.Completion M] [FiniteDimensional v.Completion M] [Algebra.IsSeparable v.Completion M], ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K L) = v), Module.finrank K L = Module.finrank v.Completion M ∧ ∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)

theorem galois_closure_restriction_hom_exists_aux {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (g : Polynomial K₀) (hg_sep : g.Separable) (hg_monic : g.Monic) (hg_irr : Irreducible g) : ∃ (φ : Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) →* Gal(g.SplittingField/K₀)), Function.Injective ⇑φ

theorem galois_closure_completion_places_exist_aux {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (g : Polynomial K₀) (hg_sep : g.Separable) (hg_monic : g.Monic) (hg_irr : Irreducible g) (L' : Type) [Field L'] [NumberField L'] [Algebra K₀ L'] [Algebra.IsSeparable K₀ L'] [FiniteDimensional K₀ L'] (w' : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L')) (hw' : Ideal.comap (algebraMap (NumberField.RingOfIntegers K₀) (NumberField.RingOfIntegers L')) w'.asIdeal = v₀.asIdeal) (hfinrank : Module.finrank K₀ L' = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M) (hiso : ∃ (x : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')) (φ : Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) →* Gal(g.SplittingField/K₀)) (hφ_inj : Function.Injective ⇑φ) [NumberField g.SplittingField] [NumberField ↥(IntermediateField.fixedField φ.range)] : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥(IntermediateField.fixedField φ.range))) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion (↥(IntermediateField.fixedField φ.range)) v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers g.SplittingField)) (halg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion g.SplittingField w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion g.SplittingField w)

theorem galois_closure_restriction_hom_exists {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (g : Polynomial K₀) (hg_sep : g.Separable) (hg_monic : g.Monic) (hg_irr : Irreducible g) : ∃ (φ : Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) →* Gal(g.SplittingField/K₀)), Function.Injective ⇑φ

theorem galois_closure_completion_places_exist {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (g : Polynomial K₀) (hg_sep : g.Separable) (hg_monic : g.Monic) (hg_irr : Irreducible g) (L' : Type) [Field L'] [NumberField L'] [Algebra K₀ L'] [Algebra.IsSeparable K₀ L'] [FiniteDimensional K₀ L'] (w' : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L')) (hw' : Ideal.comap (algebraMap (NumberField.RingOfIntegers K₀) (NumberField.RingOfIntegers L')) w'.asIdeal = v₀.asIdeal) (hfinrank : Module.finrank K₀ L' = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M) (hiso : ∃ (x : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')) (φ : Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) →* Gal(g.SplittingField/K₀)) (hφ_inj : Function.Injective ⇑φ) [NumberField g.SplittingField] [NumberField ↥(IntermediateField.fixedField φ.range)] : ∃ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers ↥(IntermediateField.fixedField φ.range))) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion (↥(IntermediateField.fixedField φ.range)) v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers g.SplittingField)) (halg : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion g.SplittingField w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion g.SplittingField w)

theorem galois_closure_of_separable_poly {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (g : Polynomial K₀) (hg_sep : g.Separable) (hg_monic : g.Monic) (hg_irr : Irreducible g) (L' : Type) [Field L'] [NumberField L'] [Algebra K₀ L'] [Algebra.IsSeparable K₀ L'] [FiniteDimensional K₀ L'] (w' : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L')) (hw' : Ideal.comap (algebraMap (NumberField.RingOfIntegers K₀) (NumberField.RingOfIntegers L')) w'.asIdeal = v₀.asIdeal) (hfinrank : Module.finrank K₀ L' = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M) (hiso : ∃ (x : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')) : ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (L : Type) (x_2 : Field L) (x_3 : NumberField L) (x_4 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x_8 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ∧ Nonempty (Gal(L/K) ≃* Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀))

theorem galois_closure_completion_exists {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] (L' : Type) (x✝ : Field L') (x✝¹ : NumberField L') (x✝² : Algebra K₀ L') : Algebra.IsSeparable K₀ L' → FiniteDimensional K₀ L' → ∀ (w' : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L')), Ideal.comap (algebraMap (NumberField.RingOfIntegers K₀) (NumberField.RingOfIntegers L')) w'.asIdeal = v₀.asIdeal → Module.finrank K₀ L' = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M → (∃ (x : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L' w')) → ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (L : Type) (x_2 : Field L) (x_3 : NumberField L) (x_4 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x_8 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ∧ Nonempty (Gal(L/K) ≃* Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀))

theorem galoisExtension_isCompletion_finitePlace {K₀ : Type} [Field K₀] [NumberField K₀] (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [Field M] [Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] : ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (L : Type) (x_2 : Field L) (x_3 : NumberField L) (x_4 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x_8 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ∧ Nonempty (Gal(L/K) ≃* Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀))

theorem algEquiv_eq_refl_of_finrank_one {F : Type u_1} {E : Type u_2} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (h : Module.finrank F E = 1) (e : Gal(E/F)) : e = AlgEquiv.refl

def galoisGroupMulEquivTrivial (K : Type u_1) (F : Type u_2) (E : Type u_3) [Field K] [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (h : Module.finrank F E = 1) : Gal(K/K) ≃* Gal(E/F)

theorem galoisExtension_isCompletion_infinitePlace {K : Type} [Field K] [NumberField K] (v : NumberField.InfinitePlace K) (M : Type u_1) [Field M] [Algebra v.Completion M] [FiniteDimensional v.Completion M] [IsGalois v.Completion M] : ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K L) = v), (∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)) ∧ Nonempty (Gal(L/K) ≃* Gal(M/v.Completion))

theorem galoisExtension_isCompletion {K₀ : Type} [Field K₀] [NumberField K₀] : (∀ (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [inst : Field M] [inst_1 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M], ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (L : Type) (x_2 : Field L) (x_3 : NumberField L) (x_4 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x_8 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ∧ Nonempty (Gal(L/K) ≃* Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀))) ∧ ∀ (v : NumberField.InfinitePlace K₀) (M : Type u_2) [inst : Field M] [inst_1 : Algebra v.Completion M] [FiniteDimensional v.Completion M] [IsGalois v.Completion M], ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K₀ L) (_ : IsGalois K₀ L) (_ : FiniteDimensional K₀ L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K₀ L) = v), (∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)) ∧ Nonempty (Gal(L/K₀) ≃* Gal(M/v.Completion))

noncomputable def commKvAlgEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] [NumberField K] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)

theorem norm_baseChange_eq {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)) (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) α) = (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (α ⊗ₜ[K] 1)

theorem trace_baseChange_eq {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)) (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) α) = (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) (α ⊗ₜ[K] 1)

def finSuccLinearEquiv' (R : Type u_3) [CommRing R] {n : ℕ} (A : Fin (n + 1) → Type u_4) [(i : Fin (n + 1)) → AddCommGroup (A i)] [(i : Fin (n + 1)) → Module R (A i)] : ((i : Fin (n + 1)) → A i) ≃ₗ[R] A 0 × ((i : Fin n) → A i.succ)

theorem norm_pi_fin' {R : Type u_3} [CommRing R] {n : ℕ} {A : Fin n → Type u_4} [(i : Fin n) → CommRing (A i)] [(i : Fin n) → Algebra R (A i)] [∀ (i : Fin n), Module.Free R (A i)] [∀ (i : Fin n), Module.Finite R (A i)] (f : (i : Fin n) → A i) : (Algebra.norm R) f = ∏ i : Fin n, (Algebra.norm R) (f i)

theorem Algebra.norm_pi_apply' {R : Type u_3} [CommRing R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {A : ι → Type u_5} [(i : ι) → CommRing (A i)] [(i : ι) → Algebra R (A i)] [∀ (i : ι), Module.Free R (A i)] [∀ (i : ι), Module.Finite R (A i)] (f : (i : ι) → A i) : (norm R) f = ∏ i : ι, (norm R) (f i)

theorem algEquiv_tmul_one_component {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (localAlg : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) (he : ∀ (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α) (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) : e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α

theorem norm_pi_eq_prod {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (localAlg : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) (he : ∀ (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α) (α : L) : (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (α ⊗ₜ[K] 1) = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)

theorem trace_single_comp_aux {R : Type u_3} [CommRing R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {A : ι → Type u_5} [(i : ι) → CommRing (A i)] [(i : ι) → Algebra R (A i)] [∀ (i : ι), Module.Free R (A i)] [∀ (i : ι), Module.Finite R (A i)] (j : ι) (f : A j →ₗ[R] A j) : (LinearMap.trace R ((i : ι) → A i)) (LinearMap.single R A j ∘ₗ f ∘ₗ LinearMap.proj j) = (LinearMap.trace R (A j)) f

theorem pi_lmul_decomp_aux {R : Type u_3} [CommRing R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {A : ι → Type u_5} [(i : ι) → CommRing (A i)] [(i : ι) → Algebra R (A i)] (f : (i : ι) → A i) : (Algebra.lmul R ((i : ι) → A i)) f = ∑ i : ι, LinearMap.single R A i ∘ₗ (Algebra.lmul R (A i)) (f i) ∘ₗ LinearMap.proj i

theorem Algebra.trace_pi_apply' {R : Type u_3} [CommRing R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {A : ι → Type u_5} [(i : ι) → CommRing (A i)] [(i : ι) → Algebra R (A i)] [∀ (i : ι), Module.Free R (A i)] [∀ (i : ι), Module.Finite R (A i)] (f : (i : ι) → A i) : (trace R ((i : ι) → A i)) f = ∑ i : ι, (trace R (A i)) (f i)

theorem trace_pi_eq_sum {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (localAlg : (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) (e : TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }) → IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w) (he : ∀ (α : L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }), e (α ⊗ₜ[K] 1) w = (algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α) (α : L) : (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (TensorProduct K L (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))) (α ⊗ₜ[K] 1) = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)

theorem norm_eq_prod_localNorm {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) α) = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)

theorem trace_eq_sum_localTrace {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) α) = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)

theorem norm_trace_completion_decomposition {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) α) = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α) ∧ (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) α) = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)

@[reducible, inline]

abbrev theorem_11_20 {K : Type} [Field K] [NumberField K] : (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (M : Type u_1) [inst : Field M] [inst_1 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M] [Algebra.IsSeparable (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M], ∃ (L : Type) (x : Field L) (x_1 : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (_ : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) w.asIdeal = v.asIdeal), Module.finrank K L = Module.finrank (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) M ∧ ∃ (x_6 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K v] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)) ∧ ∀ (v : NumberField.InfinitePlace K) (M : Type u_2) [inst : Field M] [inst_1 : Algebra v.Completion M] [FiniteDimensional v.Completion M] [Algebra.IsSeparable v.Completion M], ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K L) (_ : Algebra.IsSeparable K L) (_ : FiniteDimensional K L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K L) = v), Module.finrank K L = Module.finrank v.Completion M ∧ ∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)

@[reducible, inline]

abbrev corollary_11_22 {K₀ : Type} [Field K₀] [NumberField K₀] : (∀ (v₀ : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K₀)) (M : Type u_1) [inst : Field M] [inst_1 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [FiniteDimensional (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M] [IsGalois (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) M], ∃ (K : Type) (x : Field K) (x_1 : NumberField K) (L : Type) (x_2 : Field L) (x_3 : NumberField L) (x_4 : Algebra K L) (_ : IsGalois K L) (_ : FiniteDimensional K L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (_ : Nonempty (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v ≃+* IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀)) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) (x_8 : Algebra (IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L w)), Nonempty (M ≃ₐ[IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀] IsDedekindDomain.HeightOneSpectrum.adicCompletion L w) ∧ Nonempty (Gal(L/K) ≃* Gal(M/IsDedekindDomain.HeightOneSpectrum.adicCompletion K₀ v₀))) ∧ ∀ (v : NumberField.InfinitePlace K₀) (M : Type u_2) [inst : Field M] [inst_1 : Algebra v.Completion M] [FiniteDimensional v.Completion M] [IsGalois v.Completion M], ∃ (L : Type) (x : Field L) (_ : NumberField L) (x_2 : Algebra K₀ L) (_ : IsGalois K₀ L) (_ : FiniteDimensional K₀ L) (w : NumberField.InfinitePlace L) (_ : w.comap (algebraMap K₀ L) = v), (∃ (x_6 : Algebra v.Completion w.Completion), Nonempty (M ≃ₐ[v.Completion] w.Completion)) ∧ Nonempty (Gal(L/K₀) ≃* Gal(M/v.Completion))

@[reducible, inline]

abbrev corollary_11_24 {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)) [Fintype { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }] (α : L) : (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.norm K) α) = ∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.norm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α) ∧ (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ((Algebra.trace K L) α) = ∑ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // FinitePlace.LiesAbove w v }, (Algebra.trace (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) ((algebraMap L (IsDedekindDomain.HeightOneSpectrum.adicCompletion L ↑w)) α)