def RayClassField.lyingUnder (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)

noncomputable def RayClassField.ramificationIndex' (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : ℕ

noncomputable def RayClassField.inertiaDegree' (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : ℕ

theorem RayClassField.fiber_under_finite (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : {𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) | IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) 𝔮 = 𝔭}.Finite

theorem RayClassField.extendModulus_finite_support (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔪 : Modulus K) : {v : Place L | (match v with | Place.finite 𝔮 => ramificationIndex' K L 𝔮 * 𝔪.toFun (Place.finite (lyingUnder K L 𝔮)) | Place.infinite w => if w.IsComplex then 0 else 𝔪.toFun (Place.infinite (w.comap (algebraMap K L)))) ≠ 0}.Finite

noncomputable def RayClassField.extendModulus (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔪 : Modulus K) : Modulus L

theorem RayClassField.cgwz_rearrange {α : Type u_1} [CommGroupWithZero α] {a b c d e f : α} (ha : a ≠ 0) (hd : d ≠ 0) (he : e ≠ 0) (h : a * b * c = d * e * f) : f * a⁻¹ = b * d⁻¹ * (c * e⁻¹)

theorem RayClassField.algMap_intNorm_den_ne_zero (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L) : (algebraMap (NumberField.RingOfIntegers K) K) ((Algebra.intNorm (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ↑I.den) ≠ 0

theorem RayClassField.spanSingleton_intNorm_ne_zero (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L) : FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) ((algebraMap (NumberField.RingOfIntegers K) K) ((Algebra.intNorm (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) ↑I.den)) ≠ 0

noncomputable def RayClassField.fracRelNorm (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers L)) L →* FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K

noncomputable def RayClassField.fracIdealNorm (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] : (FracIdeal L)ˣ →* (FracIdeal K)ˣ

theorem RayClassField.fracRelNorm_coeIdeal_eq (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (J : Ideal (NumberField.RingOfIntegers L)) : (fracRelNorm K L) ↑J = ↑((Ideal.relNorm (NumberField.RingOfIntegers K)) J)

theorem RayClassField.fracIdealNorm_prime_eq (K L : Type u) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [IsGalois K L] (𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : (fracIdealNorm K L) (primeAsUnitFracIdeal L 𝔮) = primeAsUnitFracIdeal K (lyingUnder K L 𝔮) ^ inertiaDegree' K L 𝔮

theorem RayClassField.ramificationIndex'_pos (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔮 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : 0 < ramificationIndex' K L 𝔮

theorem RayClassField.norm_trivialValuation_of_all_lying_over (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (x : L) (v : FinitePlace K) (hx : x ≠ 0) (hw : ∀ (w : FinitePlace L), lyingUnder K L w = v → (IsDedekindDomain.HeightOneSpectrum.valuation L w) x = 1) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ((Algebra.norm K) x) = 1

theorem RayClassField.fracIdeal_exists_simultaneous_trivialValuation_finset {L : Type u} [Field L] [NumberField L] (I : (FracIdeal L)ˣ) (S : Finset (FinitePlace L)) (hI : ∀ w ∈ S, HasTrivialValuation I w) : ∃ x ∈ ↑I, x ≠ 0 ∧ ∀ w ∈ S, (IsDedekindDomain.HeightOneSpectrum.valuation L w) x = 1

theorem RayClassField.exists_simultaneous_trivialValuation (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (I : (FracIdeal L)ˣ) (v : FinitePlace K) (hI : ∀ (w : FinitePlace L), lyingUnder K L w = v → HasTrivialValuation I w) : ∃ x ∈ ↑I, x ≠ 0 ∧ ∀ (w : FinitePlace L), lyingUnder K L w = v → (IsDedekindDomain.HeightOneSpectrum.valuation L w) x = 1

theorem RayClassField.norm_mem_fracRelNorm (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (I : FracIdeal L) (x : L) (hx : x ∈ I) : (Algebra.norm K) x ∈ (fracRelNorm K L) I

theorem RayClassField.hasTrivialValuation_fracIdealNorm (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (I : (FracIdeal L)ˣ) (v : FinitePlace K) (hI : ∀ (w : FinitePlace L), lyingUnder K L w = v → HasTrivialValuation I w) : HasTrivialValuation ((fracIdealNorm K L) I) v

theorem RayClassField.fracIdealNorm_coprime (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) (I : (FracIdeal L)ˣ) (hI : I ∈ FracIdealsCoprime_subgroup L (extendModulus K L 𝔪)) : (fracIdealNorm K L) I ∈ FracIdealsCoprime_subgroup K 𝔪

noncomputable def RayClassField.idealNormMap (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) : FracIdealsCoprime L (extendModulus K L 𝔪) →* FracIdealsCoprime K 𝔪

noncomputable def RayClassField.NormGroup (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) : Subgroup (FracIdealsCoprime K 𝔪)

theorem RayClassField.rayGroup_le_normGroup (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) : RayGroup K 𝔪 ≤ NormGroup K L 𝔪

theorem RayClassField.idealNormMap_range_le_normGroup (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) : (idealNormMap K L 𝔪).range ≤ NormGroup K L 𝔪