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

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

def RayClassField.Place.isFinite {K : Type u_1} [Field K] [NumberField K] : Place K → Prop

structure RayClassField.Modulus (K : Type u_2) [Field K] [NumberField K] : Type u_2

• toFun : Place K → ℕ
• finite_support : {v : Place K | self.toFun v ≠ 0}.Finite
• inf_le_one (v : NumberField.InfinitePlace K) : self.toFun (Place.infinite v) ≤ 1
• complex_zero (v : NumberField.InfinitePlace K) : v.IsComplex → self.toFun (Place.infinite v) = 0

@[implicit_reducible]

instance RayClassField.instCoeFunModulusForallPlaceNat {K : Type u_1} [Field K] [NumberField K] : CoeFun (Modulus K) fun (x : Modulus K) => Place K → ℕ

def RayClassField.Modulus.finitePart {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K) → ℕ

def RayClassField.Modulus.infSupport {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Set (NumberField.InfinitePlace K)

theorem RayClassField.Modulus.infSupport_subset_real {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (v : NumberField.InfinitePlace K) : v ∈ 𝔪.infSupport → v.IsReal

structure RayClassField.SimpleModulus (K : Type u_2) [Field K] [NumberField K] : Type u_2

• finite_part : Ideal (NumberField.RingOfIntegers K)
• infinite_part : Set (NumberField.InfinitePlace K)
• real_places (v : NumberField.InfinitePlace K) : v ∈ self.infinite_part → v.IsReal

theorem RayClassField.SimpleModulus.ext_iff {K : Type u_2} {inst✝ : Field K} {inst✝¹ : NumberField K} {x y : SimpleModulus K} : x = y ↔ x.finite_part = y.finite_part ∧ x.infinite_part = y.infinite_part

theorem RayClassField.SimpleModulus.ext {K : Type u_2} {inst✝ : Field K} {inst✝¹ : NumberField K} {x y : SimpleModulus K} (finite_part : x.finite_part = y.finite_part) (infinite_part : x.infinite_part = y.infinite_part) : x = y

def RayClassField.SimpleModulus.trivial {K : Type u_1} [Field K] [NumberField K] : SimpleModulus K

noncomputable def RayClassField.Modulus.finitePartIdeal {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Ideal (NumberField.RingOfIntegers K)

def RayClassField.Modulus.dvd {K : Type u_1} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) : Prop

def RayClassField.Modulus.gcd {K : Type u_1} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) : Modulus K

def RayClassField.Modulus.lcm {K : Type u_1} [Field K] [NumberField K] (𝔪 𝔫 : Modulus K) : Modulus K

def RayClassField.Modulus.trivial {K : Type u_1} [Field K] [NumberField K] : Modulus K

@[reducible, inline]

abbrev RayClassField.FinitePlace (K : Type u_2) [Field K] [NumberField K] : Type u_2

@[reducible, inline]

abbrev RayClassField.FracIdeal (K : Type u_2) [Field K] [NumberField K] : Type u_2

def RayClassField.HasTrivialValuation {K : Type u_1} [Field K] [NumberField K] (I : (FracIdeal K)ˣ) (v : FinitePlace K) : Prop

def RayClassField.FracIdeal.IsCoprimeTo {K : Type u_1} [Field K] [NumberField K] (I : (FracIdeal K)ˣ) (v : FinitePlace K) : Prop

theorem RayClassField.hasTrivialValuation_one {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) : HasTrivialValuation 1 v

theorem RayClassField.hasTrivialValuation_mul {K : Type u_1} [Field K] [NumberField K] {a b : (FracIdeal K)ˣ} {v : FinitePlace K} (ha : HasTrivialValuation a v) (hb : HasTrivialValuation b v) : HasTrivialValuation (a * b) v

def RayClassField.FracIdealsCoprime_subgroup (K : Type u_2) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (FracIdeal K)ˣ

def RayClassField.FracIdealsCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

@[implicit_reducible]

instance RayClassField.instCommGroupFracIdealsCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : CommGroup (FracIdealsCoprime K 𝔪)

def RayClassField.IsRayGenerator {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : FracIdealsCoprime K 𝔪) : Prop

def RayClassField.RayGroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (FracIdealsCoprime K 𝔪)

def RayClassField.RayClassGroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

@[implicit_reducible]

instance RayClassField.instCommGroupRayClassGroup {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : CommGroup (RayClassGroup K 𝔪)

noncomputable def RayClassField.choosePrimeOver (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : FinitePlace K) : Ideal (NumberField.RingOfIntegers L)

instance RayClassField.choosePrimeOver_isPrime (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : FinitePlace K) : (choosePrimeOver K L 𝔭).IsPrime

theorem RayClassField.choosePrimeOver_over (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : FinitePlace K) : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (choosePrimeOver K L 𝔭) = 𝔭.asIdeal

theorem RayClassField.choosePrimeOver_ne_bot (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : FinitePlace K) : choosePrimeOver K L 𝔭 ≠ ⊥

instance RayClassField.choosePrimeOver_finite (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : FinitePlace K) : Finite (NumberField.RingOfIntegers L ⧸ choosePrimeOver K L 𝔭)

noncomputable def RayClassField.FrobeniusAutomorphism (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔭 : FinitePlace K) : Gal(L/K)

noncomputable def RayClassField.primeAsUnitFracIdeal (K : Type u) [Field K] [NumberField K] (𝔭 : FinitePlace K) : (FracIdeal K)ˣ

theorem RayClassField.primeAsUnitFracIdeal_coprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0) : primeAsUnitFracIdeal K 𝔭 ∈ FracIdealsCoprime_subgroup K 𝔪

noncomputable def RayClassField.primeCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0) : FracIdealsCoprime K 𝔪

def RayClassField.primesCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Set (FracIdealsCoprime K 𝔪)

theorem RayClassField.count_spanSingleton_eq_zero (K : Type u) [Field K] [NumberField K] (v : FinitePlace K) (x : K) (hx : x ≠ 0) (hv : (IsDedekindDomain.HeightOneSpectrum.valuation K v) x = 1) : FractionalIdeal.count K v (FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) x) = 0

theorem RayClassField.count_eq_zero_of_isCoprimeTo (K : Type u) [Field K] [NumberField K] (I : (FracIdeal K)ˣ) (v : FinitePlace K) (h : FracIdeal.IsCoprimeTo I v) : FractionalIdeal.count K v ↑I = 0

theorem RayClassField.primeCoprime_val (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0) : ↑(primeCoprime K 𝔪 𝔭 h𝔭) = primeAsUnitFracIdeal K 𝔭

theorem RayClassField.primeAsUnitFracIdeal_val (K : Type u) [Field K] [NumberField K] (𝔭 : FinitePlace K) : ↑(primeAsUnitFracIdeal K 𝔭) = ↑𝔭.asIdeal

theorem RayClassField.fracIdealsCoprime_closure_primes (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup.closure (primesCoprime K 𝔪) = ⊤

@[reducible, inline]

abbrev RayClassField.CoprimePrimes (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

noncomputable def RayClassField.freeGroupToCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : FreeGroup (CoprimePrimes K 𝔪) →* FracIdealsCoprime K 𝔪

noncomputable def RayClassField.freeGroupToGal (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔪 : Modulus K) : FreeGroup (CoprimePrimes K 𝔪) →* Gal(L/K)

theorem RayClassField.primesCoprime_eq_range (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : primesCoprime K 𝔪 = Set.range fun (p : CoprimePrimes K 𝔪) => primeCoprime K 𝔪 ↑p ⋯

theorem RayClassField.freeGroupToCoprime_surjective (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(freeGroupToCoprime K 𝔪)

theorem RayClassField.fractionalIdeal_mulEquiv_finsupp_primeAsUnit (K : Type u) [Field K] [NumberField K] (p : FinitePlace K) : (fractionalIdeal_mulEquiv_finsupp K) (primeAsUnitFracIdeal K p) = Multiplicative.ofAdd fun₀ | p => 1

theorem RayClassField.freeGroupToCoprime_ker_le_commutator (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : (freeGroupToCoprime K 𝔪).ker ≤ commutator (FreeGroup (CoprimePrimes K 𝔪))

theorem RayClassField.artinMap_ker_condition (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) : (freeGroupToCoprime K 𝔪).ker ≤ (freeGroupToGal K L 𝔪).ker

theorem RayClassField.artinMapExists (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) : ∃ (ψ : FracIdealsCoprime K 𝔪 →* Gal(L/K)), ∀ (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0), ψ (primeCoprime K 𝔪 𝔭 h𝔭) = FrobeniusAutomorphism K L 𝔭

noncomputable def RayClassField.ArtinMap (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) : FracIdealsCoprime K 𝔪 →* Gal(L/K)

theorem RayClassField.artinMap_at_prime_eq_frobenius (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0) : (ArtinMap K L 𝔪) (primeCoprime K 𝔪 𝔭 h𝔭) = FrobeniusAutomorphism K L 𝔭

structure RayClassField.IsRayClassField (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) : Prop

• finiteDimensional : FiniteDimensional K L
• unramified_outside (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : 𝔪.toFun (Place.finite 𝔭) = 0 → ∀ (𝔔 : Ideal (NumberField.RingOfIntegers L)) [inst : 𝔔.IsPrime], 𝔔.LiesOver 𝔭.asIdeal → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) 𝔔
• kernel_eq_ray_group : (ArtinMap K L 𝔪).ker = RayGroup K 𝔪

theorem RayClassField.restrictNormalHom_isArithFrobAt (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (Q_M : Ideal (NumberField.RingOfIntegers M)) [Q_M.IsPrime] [Finite (NumberField.RingOfIntegers M ⧸ Q_M)] (σ : Gal(M/K)) (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ Q_M) : IsArithFrobAt (NumberField.RingOfIntegers K) ((AlgEquiv.restrictNormalHom L) σ) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) Q_M)

theorem RayClassField.choosePrimeOver_comap_ne_bot (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (𝔭 : FinitePlace K) : Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭) ≠ ⊥

instance RayClassField.choosePrimeOver_comap_isPrime (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (𝔭 : FinitePlace K) : (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭)).IsPrime

instance RayClassField.choosePrimeOver_comap_finite (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (𝔭 : FinitePlace K) : Finite (NumberField.RingOfIntegers L ⧸ Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭))

instance RayClassField.galAutFaithfulSMulRingOfIntegers (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] : FaithfulSMul Gal(L/K) (NumberField.RingOfIntegers L)

theorem RayClassField.choosePrimeOver_comap_over (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (𝔭 : FinitePlace K) : Ideal.comap (algebraMap (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭)) = 𝔭.asIdeal

theorem RayClassField.prop_7_13_restrictNormalHom_arithFrobAt (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] (𝔭 : FinitePlace K) [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭))] : (AlgEquiv.restrictNormalHom L) (arithFrobAt (NumberField.RingOfIntegers K) Gal(M/K) (choosePrimeOver K M 𝔭)) = arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭))

theorem RayClassField.arithFrobAt_eq_of_under_eq (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] [KroneckerWeber.IsAbelianExtension K L] (Q Q' : Ideal (NumberField.RingOfIntegers L)) [Q.IsPrime] [Finite (NumberField.RingOfIntegers L ⧸ Q)] [Q'.IsPrime] [Finite (NumberField.RingOfIntegers L ⧸ Q')] (h : Ideal.under (NumberField.RingOfIntegers K) Q = Ideal.under (NumberField.RingOfIntegers K) Q') : arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) Q = arithFrobAt (NumberField.RingOfIntegers K) Gal(L/K) Q'

theorem RayClassField.restrictNormalHom_frobeniusAutomorphism (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsGalois K L] [IsGalois K M] [IsScalarTower K L M] [KroneckerWeber.IsAbelianExtension K L] (𝔭 : FinitePlace K) [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭))] : (AlgEquiv.restrictNormalHom L) (FrobeniusAutomorphism K M 𝔭) = FrobeniusAutomorphism K L 𝔭

theorem RayClassField.prop_7_22_artinMap_at_prime (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [KroneckerWeber.IsAbelianExtension K L] [KroneckerWeber.IsAbelianExtension K M] [IsScalarTower K L M] (𝔪 : Modulus K) (𝔭 : FinitePlace K) (h𝔭 : 𝔪.toFun (Place.finite 𝔭) = 0) [Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) (Ideal.comap (algebraMap (NumberField.RingOfIntegers L) (NumberField.RingOfIntegers M)) (choosePrimeOver K M 𝔭))] : (AlgEquiv.restrictNormalHom L) ((ArtinMap K M 𝔪) (primeCoprime K 𝔪 𝔭 h𝔭)) = (ArtinMap K L 𝔪) (primeCoprime K 𝔪 𝔭 h𝔭)

theorem RayClassField.proposition_21_1_artin_commutes (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [KroneckerWeber.IsAbelianExtension K L] [KroneckerWeber.IsAbelianExtension K M] [IsScalarTower K L M] (𝔪 : Modulus K) (hdiv : ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), 𝔪.toFun (Place.finite 𝔭) = 0 → ∀ (𝔔 : Ideal (NumberField.RingOfIntegers L)) [inst : 𝔔.IsPrime], 𝔔.LiesOver 𝔭.asIdeal → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) 𝔔) (I : FracIdealsCoprime K 𝔪) : (AlgEquiv.restrictNormalHom L) ((ArtinMap K M 𝔪) I) = (ArtinMap K L 𝔪) I

noncomputable def RayClassField.Modulus.infSupportFinset {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Finset (NumberField.InfinitePlace K)

def RayClassField.UnitsCoprime_subgroup' (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup Kˣ

def RayClassField.UnitsCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

theorem RayClassField.embedding_im_zero {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : K) : (w.embedding x).im = 0

def RayClassField.UnitsCongruent_subgroup' (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup Kˣ

def RayClassField.UnitsCongruent (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

def RayClassField.UnitsCongruent_in_UnitsCoprime (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup ↥(UnitsCoprime_subgroup' K 𝔪)

def RayClassField.QuotientUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

@[implicit_reducible]

instance RayClassField.instCommGroupQuotientUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : CommGroup (QuotientUnits K 𝔪)

def RayClassField.UnitsInCongruenceSubgroup_subgroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Subgroup (NumberField.RingOfIntegers K)ˣ

def RayClassField.UnitsInCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

@[implicit_reducible]

instance RayClassField.instCommGroupUnitsInCongruenceSubgroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : CommGroup (UnitsInCongruenceSubgroup K 𝔪)

def RayClassField.SignsTimesUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Type u

@[implicit_reducible]

noncomputable instance RayClassField.instCommGroupSignsTimesUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : CommGroup (SignsTimesUnits K 𝔪)

noncomputable instance RayClassField.instFintypeSignsTimesUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Fintype (SignsTimesUnits K 𝔪)

theorem RayClassField.Modulus.finitePartIdeal_ne_bot {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : 𝔪.finitePartIdeal ≠ ⊥

theorem RayClassField.lemma_21_7_ideal_class_coprime_rep (A : Type u_2) [CommRing A] [IsDomain A] [IsDedekindDomain A] (𝔞 : Ideal A) (c : ClassGroup A) (h𝔞 : 𝔞 ≠ ⊥) : ∃ (I : ↥(nonZeroDivisors (Ideal A))), ClassGroup.mk0 I = c ∧ ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum A), 𝔭.asIdeal ∣ 𝔞 → ¬𝔭.asIdeal ∣ ↑I

def RayClassField.exactSeq_map1 {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : UnitsInCongruenceSubgroup K 𝔪 →* (NumberField.RingOfIntegers K)ˣ

def RayClassField.okUnitsToKUnits {K : Type u_1} [Field K] : (NumberField.RingOfIntegers K)ˣ →* Kˣ

theorem RayClassField.valuation_algebraMap_unit_eq_one {K : Type u_1} [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (u : (NumberField.RingOfIntegers K)ˣ) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ((algebraMap (NumberField.RingOfIntegers K) K) ↑u) = 1

theorem RayClassField.okUnitsInUnitsCoprime {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K)ˣ) : okUnitsToKUnits u ∈ UnitsCoprime_subgroup' K 𝔪

def RayClassField.okUnitsToUnitsCoprime {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (NumberField.RingOfIntegers K)ˣ →* ↥(UnitsCoprime_subgroup' K 𝔪)

def RayClassField.exactSeq_map2 {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (NumberField.RingOfIntegers K)ˣ →* QuotientUnits K 𝔪

theorem RayClassField.toPrincipalIdeal_mem_FracIdealsCoprime {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (α : Kˣ) (hα : α ∈ UnitsCoprime_subgroup' K 𝔪) : (toPrincipalIdeal (NumberField.RingOfIntegers K) K) α ∈ FracIdealsCoprime_subgroup K 𝔪

noncomputable def RayClassField.principalIdealMap {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : ↥(UnitsCoprime_subgroup' K 𝔪) →* FracIdealsCoprime K 𝔪

theorem RayClassField.principalIdealMap_val {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (α : ↥(UnitsCoprime_subgroup' K 𝔪)) : ↑↑((principalIdealMap 𝔪) α) = FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) ↑↑α

theorem RayClassField.principalIdealMap_congruent_to_ray {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (α : ↥(UnitsCoprime_subgroup' K 𝔪)) (hα : ↑α ∈ UnitsCongruent_subgroup' K 𝔪) : (principalIdealMap 𝔪) α ∈ RayGroup K 𝔪

noncomputable def RayClassField.exactSeq_map3 {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : QuotientUnits K 𝔪 →* RayClassGroup K 𝔪

noncomputable def RayClassField.exactSeq_map4 {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : RayClassGroup K 𝔪 →* ClassGroup (NumberField.RingOfIntegers K)

theorem RayClassField.exactSeq_exact_at_units {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (exactSeq_map1 𝔪).range = (exactSeq_map2 𝔪).ker

theorem RayClassField.toPrincipalIdeal_algebraMap_unit' {K : Type u_1} [Field K] [NumberField K] (u : (NumberField.RingOfIntegers K)ˣ) : (toPrincipalIdeal (NumberField.RingOfIntegers K) K) ((Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) u) = 1

theorem RayClassField.principalIdealMap_okUnitsToUnitsCoprime_eq_one' {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K)ˣ) : (principalIdealMap 𝔪) ((okUnitsToUnitsCoprime 𝔪) u) = 1

theorem RayClassField.toPrincipalIdeal_eq_exists_unit' {K : Type u_1} [Field K] [NumberField K] (x y : Kˣ) (h : (toPrincipalIdeal (NumberField.RingOfIntegers K) K) x = (toPrincipalIdeal (NumberField.RingOfIntegers K) K) y) : ∃ (u : (NumberField.RingOfIntegers K)ˣ), x = (Units.map ↑(algebraMap (NumberField.RingOfIntegers K) K)) u * y

theorem RayClassField.valuation_eq_one_of_spanSingleton_coprime' {K : Type u_1} [Field K] [NumberField K] (v : FinitePlace K) (α : Kˣ) (h1 : HasTrivialValuation ((toPrincipalIdeal (NumberField.RingOfIntegers K) K) α) v) (h2 : HasTrivialValuation ((toPrincipalIdeal (NumberField.RingOfIntegers K) K) α)⁻¹ v) : (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑α = 1

theorem RayClassField.rayGroup_le_map_congruent' {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : RayGroup K 𝔪 ≤ Subgroup.map (principalIdealMap 𝔪) (UnitsCongruent_in_UnitsCoprime K 𝔪)

theorem RayClassField.exactSeq_exact_at_quotient {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (exactSeq_map2 𝔪).range = (exactSeq_map3 𝔪).ker

theorem RayClassField.exactSeq_exact_at_ray_class {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : (exactSeq_map3 𝔪).range = (exactSeq_map4 𝔪).ker

theorem RayClassField.mk0_mem_FracIdealsCoprime_of_coprime {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (hI : ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), 𝔭.asIdeal ∣ 𝔪.finitePartIdeal → ¬𝔭.asIdeal ∣ ↑I) : (FractionalIdeal.mk0 K) I ∈ FracIdealsCoprime_subgroup K 𝔪

theorem RayClassField.classGroup_mk_comp_subtype_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(ClassGroup.mk.comp (FracIdealsCoprime_subgroup K 𝔪).subtype)

theorem RayClassField.exactSeq_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(exactSeq_map4 𝔪)

theorem RayClassField.Modulus.infSupportFinset_isReal {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) {w : NumberField.InfinitePlace K} (hw : w ∈ 𝔪.infSupportFinset) : w.IsReal

theorem RayClassField.embedding_re_ne_zero {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (a : Kˣ) : (w.embedding ↑a).re ≠ 0

noncomputable def RayClassField.signAtPlace {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (_hw : w.IsReal) (α : Kˣ) : ZMod 2

theorem RayClassField.signAtPlace_mul {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (a b : Kˣ) : signAtPlace hw (a * b) = signAtPlace hw a + signAtPlace hw b

theorem RayClassField.signAtPlace_eq_zero_iff {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (α : Kˣ) : signAtPlace hw α = 0 ↔ 0 < (w.embedding ↑α).re

noncomputable def RayClassField.signMapHom (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : ↥(UnitsCoprime_subgroup' K 𝔪) →* ↥𝔪.infSupportFinset → Multiplicative (ZMod 2)

theorem RayClassField.coprime_rep_exists {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (α : ↥(UnitsCoprime_subgroup' K 𝔪)) : ∃ (a : NumberField.RingOfIntegers K) (b : NumberField.RingOfIntegers K), IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) a) ∧ IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) b) ∧ (algebraMap (NumberField.RingOfIntegers K) K) a / (algebraMap (NumberField.RingOfIntegers K) K) b = ↑↑α

noncomputable def RayClassField.finitePartMapFn (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (α : ↥(UnitsCoprime_subgroup' K 𝔪)) : (NumberField.RingOfIntegers K ⧸ 𝔪.finitePartIdeal)ˣ

theorem RayClassField.coprime_rep_well_def {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) {a b c d : NumberField.RingOfIntegers K} (ha : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) a)) (hb : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) b)) (hc : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) c)) (hd : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) d)) (hab : (algebraMap (NumberField.RingOfIntegers K) K) a / (algebraMap (NumberField.RingOfIntegers K) K) b = (algebraMap (NumberField.RingOfIntegers K) K) c / (algebraMap (NumberField.RingOfIntegers K) K) d) : ha.unit * hb.unit⁻¹ = hc.unit * hd.unit⁻¹

noncomputable def RayClassField.finitePartMapHom (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : ↥(UnitsCoprime_subgroup' K 𝔪) →* (NumberField.RingOfIntegers K ⧸ 𝔪.finitePartIdeal)ˣ

theorem RayClassField.finset_prod_ideal_le_factor {R : Type u_2} [CommRing R] {ι : Type u_3} [DecidableEq ι] (S : Finset ι) (f : ι → Ideal R) (j : ι) (hj : j ∈ S) : S.prod f ≤ f j

theorem RayClassField.unit_mod_ideal_not_in_prime {R : Type u_2} [CommRing R] {I 𝔭 : Ideal R} (hI𝔭 : I ≤ 𝔭) (h𝔭 : 𝔭 ≠ ⊤) {b : R} (hb : IsUnit ((Ideal.Quotient.mk I) b)) : b ∉ 𝔭

theorem RayClassField.coprime_rep_unit_eq_one_iff {K : Type u_1} [Field K] [NumberField K] {α : Kˣ} (𝔪 : Modulus K) {a b : NumberField.RingOfIntegers K} (ha : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) a)) (hb : IsUnit ((Ideal.Quotient.mk 𝔪.finitePartIdeal) b)) (hab : (algebraMap (NumberField.RingOfIntegers K) K) a / (algebraMap (NumberField.RingOfIntegers K) K) b = ↑α) : ha.unit * hb.unit⁻¹ = 1 ↔ ∀ (v : FinitePlace K), 𝔪.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑α - 1) ≤ ↑(Multiplicative.ofAdd (-↑(𝔪.toFun (Place.finite v))))

theorem RayClassField.finitePartMapHom_ker_iff {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (α : ↥(UnitsCoprime_subgroup' K 𝔪)) : (finitePartMapHom K 𝔪) α = 1 ↔ ∀ (v : FinitePlace K), 𝔪.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑↑α - 1) ≤ ↑(Multiplicative.ofAdd (-↑(𝔪.toFun (Place.finite v))))

theorem RayClassField.weak_approx_nonzero_with_val_and_sign {K : Type u_2} [Field K] [NumberField K] (𝔪 : Modulus K) (pos : ↥𝔪.infSupportFinset → Prop) [DecidablePred pos] : ∃ (x : K) (_ : x ≠ 0), (∀ (v : FinitePlace K), 𝔪.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) x = 1) ∧ ∀ (w : NumberField.InfinitePlace K) (hw : w ∈ 𝔪.infSupportFinset), (pos ⟨w, hw⟩ → 0 < (w.embedding x).re) ∧ (¬pos ⟨w, hw⟩ → (w.embedding x).re < 0)

theorem RayClassField.weak_approx_sign_coprime {K : Type u_2} [Field K] [NumberField K] (𝔪 : Modulus K) (s : ↥𝔪.infSupportFinset → Multiplicative (ZMod 2)) : ∃ (α : Kˣ), (∀ (v : FinitePlace K), 𝔪.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑α = 1) ∧ ∀ (w : NumberField.InfinitePlace K) (hw : w ∈ 𝔪.infSupportFinset), Multiplicative.ofAdd (signAtPlace ⋯ α) = s ⟨w, hw⟩

theorem RayClassField.signMapHom_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑(signMapHom K 𝔪)

theorem RayClassField.signMapHom_surjective.signMapHom_surjective_aux {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (s : ↥𝔪.infSupportFinset → Multiplicative (ZMod 2)) : ∃ (α : ↥(UnitsCoprime_subgroup' K 𝔪)), (signMapHom K 𝔪) α = s

theorem RayClassField.weak_approx_coprime_sign_finitePart {K : Type u_2} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K ⧸ 𝔪.finitePartIdeal)ˣ) : ∃ (α : ↥(UnitsCoprime_subgroup' K 𝔪)), (signMapHom K 𝔪) α = 1 ∧ (finitePartMapHom K 𝔪) α = u

theorem RayClassField.finitePartMapHom_surj_on_ker_sign {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) (u : (NumberField.RingOfIntegers K ⧸ 𝔪.finitePartIdeal)ˣ) : ∃ (α : ↥(UnitsCoprime_subgroup' K 𝔪)), (signMapHom K 𝔪) α = 1 ∧ (finitePartMapHom K 𝔪) α = u

theorem RayClassField.signTimesFinitePart_surjective {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Function.Surjective ⇑((signMapHom K 𝔪).prod (finitePartMapHom K 𝔪))

theorem RayClassField.finite_part_map_exists {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : ∃ (f : ↥(UnitsCoprime_subgroup' K 𝔪) →* (NumberField.RingOfIntegers K ⧸ 𝔪.finitePartIdeal)ˣ), (∀ (α : ↥(UnitsCoprime_subgroup' K 𝔪)), f α = 1 ↔ ∀ (v : FinitePlace K), 𝔪.toFun (Place.finite v) ≠ 0 → (IsDedekindDomain.HeightOneSpectrum.valuation K v) (↑↑α - 1) ≤ ↑(Multiplicative.ofAdd (-↑(𝔪.toFun (Place.finite v))))) ∧ Function.Surjective ⇑((signMapHom K 𝔪).prod f)

theorem RayClassField.theorem_21_8_quotient_iso {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nonempty (QuotientUnits K 𝔪 ≃* SignsTimesUnits K 𝔪)

@[implicit_reducible]

noncomputable instance RayClassField.instFintypeQuotientUnits (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Fintype (QuotientUnits K 𝔪)

noncomputable instance RayClassField.instFintypeRayClassGroup (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : Fintype (RayClassGroup K 𝔪)

theorem RayClassField.corollary_21_9_ray_class_number {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nat.card (RayClassGroup K 𝔪) * (UnitsInCongruenceSubgroup_subgroup K 𝔪).index = Nat.card (SignsTimesUnits K 𝔪) * Nat.card (ClassGroup (NumberField.RingOfIntegers K))

theorem RayClassField.corollary_21_9_class_dvd_ray {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Fintype.card (ClassGroup (NumberField.RingOfIntegers K)) ∣ Fintype.card (RayClassGroup K 𝔪)

theorem RayClassField.corollary_21_9_ray_dvd {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Fintype.card (RayClassGroup K 𝔪) ∣ Fintype.card (ClassGroup (NumberField.RingOfIntegers K)) * Fintype.card (SignsTimesUnits K 𝔪)

theorem RayClassField.corollary_21_9 {K : Type u_1} [Field K] [NumberField K] (𝔪 : Modulus K) : Nat.card (RayClassGroup K 𝔪) * (UnitsInCongruenceSubgroup_subgroup K 𝔪).index = Nat.card (SignsTimesUnits K 𝔪) * Nat.card (ClassGroup (NumberField.RingOfIntegers K)) ∧ Fintype.card (ClassGroup (NumberField.RingOfIntegers K)) ∣ Fintype.card (RayClassGroup K 𝔪) ∧ Fintype.card (RayClassGroup K 𝔪) ∣ Fintype.card (ClassGroup (NumberField.RingOfIntegers K)) * Fintype.card (SignsTimesUnits K 𝔪)

@[reducible, inline]

abbrev RayClassField.Prime' (K : Type u_2) [Field K] [NumberField K] : Type u_2

noncomputable def RayClassField.partialDedekindZeta (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) : ℂ → ℂ

theorem RayClassField.eulerFactor_analyticAt_one {K : Type u_2} [Field K] [NumberField K] (𝔭 : Prime' K) : AnalyticAt ℂ (fun (s : ℂ) => (1 - ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s))⁻¹) 1

theorem RayClassField.dedekindZeta_sub_one_mul_analytic_aux (K : Type u_2) [Field K] [NumberField K] : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 1 ∧ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s) =ᶠ[nhds 1] g

theorem RayClassField.dedekindZeta_sub_one_mul_analyticAt (K : Type u_2) [Field K] [NumberField K] : AnalyticAt ℂ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s) 1

theorem RayClassField.partialDedekindZeta_factorization_near_one {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : ¬S.Finite) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 1 ∧ (fun (s : ℂ) => (s - 1) * NumberField.dedekindZeta K s * g s) =ᶠ[nhds 1] fun (s : ℂ) => (s - 1) * partialDedekindZeta K S s

theorem RayClassField.partialDedekindZeta_simple_pole_at_one_infinite {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : ¬S.Finite) : AnalyticAt ℂ (fun (s : ℂ) => (s - 1) * partialDedekindZeta K S s) 1

theorem RayClassField.partialDedekindZeta_simple_pole_at_one {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) : AnalyticAt ℂ (fun (s : ℂ) => (s - 1) * partialDedekindZeta K S s) 1

theorem RayClassField.partialDedekindZeta_meromorphicAt_infinite {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : S.Infinite) : MeromorphicAt (partialDedekindZeta K S) 1

theorem RayClassField.partialDedekindZeta_meromorphicAt {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) : MeromorphicAt (partialDedekindZeta K S) 1

theorem RayClassField.partialDedekindZeta_order_ge_neg_one {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) : ↑(-1) ≤ meromorphicOrderAt (partialDedekindZeta K S) 1

def RayClassField.HasMeromorphicContinuationWithPoleOrder (f : ℂ → ℂ) (m : ℤ) : Prop

theorem RayClassField.partialDedekindZeta_poleOrder_le {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {n : ℕ+} {m : ℤ} (h : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K S ^ ↑n) m) : m ≤ ↑↑n

def RayClassField.HasPolarDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) : Prop

def RayClassField.HasDirichletDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) : Prop

def RayClassField.HasNaturalDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) : Prop

theorem RayClassField.hasPolarDensity_unique {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ₁ ρ₂ : ℚ} (h₁ : HasPolarDensity K S ρ₁) (h₂ : HasPolarDensity K S ρ₂) : ρ₁ = ρ₂

theorem RayClassField.hasDirichletDensity_unique {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ₁ ρ₂ : ℚ} (h₁ : HasDirichletDensity K S ρ₁) (h₂ : HasDirichletDensity K S ρ₂) : ρ₁ = ρ₂

theorem RayClassField.hasNaturalDensity_unique {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ₁ ρ₂ : ℚ} (h₁ : HasNaturalDensity K S ρ₁) (h₂ : HasNaturalDensity K S ρ₂) : ρ₁ = ρ₂

theorem RayClassField.meromorphic_poleOrder_realLog_limit (f : ℂ → ℂ) (m : ℤ) (hm : HasMeromorphicContinuationWithPoleOrder f m) : ∃ (C : ℝ), Filter.Tendsto (fun (s : ℝ) => Real.log ‖f ↑s‖ + ↑m * Real.log (s - 1)) (nhdsWithin 1 (Set.Ioi 1)) (nhds C)

instance RayClassField.instFiniteIdealNorm' (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Finite { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

instance RayClassField.instFinitePrimesNorm' (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Finite { 𝔭 : Prime' K // Ideal.absNorm 𝔭.asIdeal = n }

theorem RayClassField.card_primes_le_card_ideals' (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Nat.card { 𝔭 : Prime' K // Ideal.absNorm 𝔭.asIdeal = n } ≤ Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

theorem RayClassField.ideal_count_rpow_summable' (K : Type u_2) [Field K] [NumberField K] (σ : ℝ) (hσ : 1 < σ) : Summable fun (n : ℕ) => ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }) * ↑n ^ (-σ)

theorem RayClassField.summable_primeIdeal_absNorm_rpow' (K : Type u_2) [Field K] [NumberField K] (σ : ℝ) (hσ : 1 < σ) : Summable fun (𝔭 : Prime' K) => ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-σ)

theorem RayClassField.partialDedekindZeta_multipliable {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (s : ℂ) (hs : 1 < s.re) : Multipliable fun (𝔭 : ↑S) => (1 - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s))⁻¹

theorem RayClassField.partialDedekindZeta_log_norm_eq_tsum {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) {s : ℝ} (hs : 1 < s) : Real.log ‖partialDedekindZeta K S ↑s‖ = ∑' (𝔭 : ↑S), -Real.log (1 - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) ∧ (Summable fun (𝔭 : ↑S) => -Real.log (1 - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s))) ∧ Summable fun (𝔭 : ↑S) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

instance RayClassField.instFiniteIdealNorm_rl (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Finite { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

instance RayClassField.instFinitePrimesNorm_rl (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Finite { 𝔭 : Prime' K // Ideal.absNorm 𝔭.asIdeal = n }

theorem RayClassField.card_primes_le_card_ideals_rl (K : Type u_2) [Field K] [NumberField K] (n : ℕ) : Nat.card { 𝔭 : Prime' K // Ideal.absNorm 𝔭.asIdeal = n } ≤ Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }

theorem RayClassField.ideal_count_rpow_summable_rl (K : Type u_2) [Field K] [NumberField K] (σ : ℝ) (hσ : 1 < σ) : Summable fun (n : ℕ) => ↑(Nat.card { I : Ideal (NumberField.RingOfIntegers K) // Ideal.absNorm I = n }) * ↑n ^ (-σ)

theorem RayClassField.summable_primeIdeal_absNorm_rpow_rl (K : Type u_2) [Field K] [NumberField K] (σ : ℝ) (hσ : 1 < σ) : Summable fun (𝔭 : Prime' K) => ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-σ)

theorem RayClassField.partialDedekindZeta_eulerProductLog_remainder_limit {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) : ∃ (C : ℝ), Filter.Tendsto (fun (s : ℝ) => ∑' (𝔭 : ↑S), (-Real.log (1 - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s))) (nhdsWithin 1 (Set.Ioi 1)) (nhds C)

theorem RayClassField.partialDedekindZeta_eulerProductLog {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) : ∃ (C : ℝ), Filter.Tendsto (fun (s : ℝ) => Real.log ‖partialDedekindZeta K S ↑s‖ - ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) (nhdsWithin 1 (Set.Ioi 1)) (nhds C)

theorem RayClassField.eulerProduct_log_asymptotic {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {n : ℕ+} {m : ℤ} (hm : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K S ^ ↑n) m) : ∃ (C : ℝ), Filter.Tendsto (fun (s : ℝ) => ↑↑n * ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s) - ↑m * Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds C)

theorem RayClassField.poleOrder_implies_dirichletDensity_limit {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {n : ℕ+} {m : ℤ} (hm : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K S ^ ↑n) m) : Filter.Tendsto (fun (s : ℝ) => (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) / Real.log (1 / (s - 1))) (nhdsWithin 1 (Set.Ioi 1)) (nhds (↑m / ↑↑n))

theorem RayClassField.partialDedekindZeta_poleOrder_nonneg {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {n : ℕ+} {m : ℤ} (h : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K S ^ ↑n) m) : 0 ≤ m

theorem RayClassField.polar_implies_dirichlet {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} (h : HasPolarDensity K S ρ) : HasDirichletDensity K S ρ

theorem RayClassField.hasPolarDensity_nonneg {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} (h : HasPolarDensity K S ρ) : 0 ≤ ρ

theorem RayClassField.hasPolarDensity_le_one {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} (h : HasPolarDensity K S ρ) : ρ ≤ 1

noncomputable def RayClassField.PolarDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) : Option ℚ

noncomputable def RayClassField.DirichletDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) : Option ℚ

noncomputable def RayClassField.NaturalDensity (K : Type u_2) [Field K] [NumberField K] (S : Set (Prime' K)) : Option ℚ

theorem RayClassField.polarDensity_eq_some_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} : PolarDensity K S = some ρ ↔ HasPolarDensity K S ρ

theorem RayClassField.dirichletDensity_eq_some_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} : DirichletDensity K S = some ρ ↔ HasDirichletDensity K S ρ

theorem RayClassField.naturalDensity_eq_some_iff {K : Type u_1} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} : NaturalDensity K S = some ρ ↔ HasNaturalDensity K S ρ

theorem RayClassField.proposition_21_12_polar_eq_dirichlet {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) (hρ : PolarDensity K S = some ρ) : DirichletDensity K S = some ρ ∧ 0 ≤ ρ ∧ ρ ≤ 1

theorem RayClassField.ps9_natural_implies_dirichlet {K : Type u_2} [Field K] [NumberField K] {S : Set (Prime' K)} {ρ : ℚ} (h : HasNaturalDensity K S ρ) : HasDirichletDensity K S ρ

theorem RayClassField.ps9_natural_eq_dirichlet {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ_nat ρ_dir : ℚ) (hnat : NaturalDensity K S = some ρ_nat) (hdir : DirichletDensity K S = some ρ_dir) : ρ_nat = ρ_dir

theorem RayClassField.corollary_21_13_polar_eq_natural {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ_polar ρ_natural : ℚ) (hpolar : PolarDensity K S = some ρ_polar) (hnatural : NaturalDensity K S = some ρ_natural) : ρ_polar = ρ_natural

def RayClassField.IsDegreeOne {K : Type u_1} [Field K] [NumberField K] (𝔭 : Prime' K) : Prop

theorem RayClassField.proposition_21_14a_finite {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : S.Finite) : PolarDensity K S = some 0

theorem RayClassField.partialDedekindZeta_univ_order (K : Type u_2) [Field K] [NumberField K] : meromorphicOrderAt (partialDedekindZeta K Set.univ) 1 = ↑(-1)

theorem RayClassField.partialDedekindZeta_disjoint_mul (K : Type u_2) [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : Disjoint S T) : (fun (s : ℂ) => partialDedekindZeta K S s * partialDedekindZeta K T s) =ᶠ[nhdsWithin 1 {1}ᶜ] partialDedekindZeta K (S ∪ T)

theorem RayClassField.partialDedekindZeta_cofinite_order {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : (Set.univ \ S).Finite) : meromorphicOrderAt (partialDedekindZeta K S) 1 = ↑(-1)

theorem RayClassField.proposition_21_14a_cofinite {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : (Set.univ \ S).Finite) : PolarDensity K S = some 1

theorem RayClassField.partialDedekindZeta_dirichletSeries_summable {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (s : ℝ) (hs : 1 < s) : Summable fun (𝔭 : ↑S) => ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

theorem RayClassField.proposition_21_14b_mono {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : S ⊆ T) (ρS ρT : ℚ) (hS : PolarDensity K S = some ρS) (hT : PolarDensity K T = some ρT) : ρS ≤ ρT

theorem RayClassField.HasMeromorphicContinuationWithPoleOrder_mul {f g : ℂ → ℂ} {m₁ m₂ : ℤ} (hf : HasMeromorphicContinuationWithPoleOrder f m₁) (hg : HasMeromorphicContinuationWithPoleOrder g m₂) : HasMeromorphicContinuationWithPoleOrder (f * g) (m₁ + m₂)

theorem RayClassField.HasMeromorphicContinuationWithPoleOrder_pow {f : ℂ → ℂ} {m : ℤ} {n : ℕ} (hf : HasMeromorphicContinuationWithPoleOrder f m) : HasMeromorphicContinuationWithPoleOrder (f ^ n) (m * ↑n)

theorem RayClassField.partialDedekindZeta_mul_of_disjoint {K : Type u_2} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : Disjoint S T) : partialDedekindZeta K (S ∪ T) =ᶠ[nhdsWithin 1 {1}ᶜ] partialDedekindZeta K S * partialDedekindZeta K T

theorem RayClassField.partialDedekindZeta_eulerProduct_factorization {K : Type u_2} [Field K] [NumberField K] (S T : Set (Prime' K)) (n₁ n₂ : ℕ) (hST : Disjoint S T) : partialDedekindZeta K (S ∪ T) ^ (n₁ * n₂) =ᶠ[nhdsWithin 1 {1}ᶜ] (partialDedekindZeta K S ^ n₁) ^ n₂ * (partialDedekindZeta K T ^ n₂) ^ n₁

theorem RayClassField.partialDedekindZeta_finite_meromorphicOrderAt_zero {K : Type u_2} [Field K] [NumberField K] (S : Set (Prime' K)) (hS : S.Finite) : meromorphicOrderAt (partialDedekindZeta K S) 1 = 0

theorem RayClassField.partialDedekindZeta_meromorphicOrderAt_factorization {K : Type u_2} [Field K] [NumberField K] (S T : Set (Prime' K)) (n₁ n₂ : ℕ) (hST : (S ∩ T).Finite) : meromorphicOrderAt (partialDedekindZeta K (S ∪ T) ^ (n₁ * n₂)) 1 = meromorphicOrderAt ((partialDedekindZeta K S ^ n₁) ^ n₂ * (partialDedekindZeta K T ^ n₂) ^ n₁) 1

theorem RayClassField.partialDedekindZeta_poleOrder_union {K : Type u_2} [Field K] [NumberField K] {S T : Set (Prime' K)} {n₁ n₂ : ℕ+} {m₁ m₂ : ℤ} (hST : (S ∩ T).Finite) (hS : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K S ^ ↑n₁) m₁) (hT : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K T ^ ↑n₂) m₂) : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K (S ∪ T) ^ ↑(n₁ * n₂)) (m₁ * ↑↑n₂ + m₂ * ↑↑n₁)

theorem RayClassField.proposition_21_14c_additive {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : (S ∩ T).Finite) (ρS ρT : ℚ) (hS : PolarDensity K S = some ρS) (hT : PolarDensity K T = some ρT) : PolarDensity K (S ∪ T) = some (ρS + ρT)

theorem RayClassField.proposition_21_14c_additive_case2 {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : (S ∩ T).Finite) (ρS ρ_union : ℚ) (hS : PolarDensity K S = some ρS) (hU : PolarDensity K (S ∪ T) = some ρ_union) : PolarDensity K T = some (ρ_union - ρS)

theorem RayClassField.proposition_21_14c_additive_case3 {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : (S ∩ T).Finite) (ρT ρ_union : ℚ) (hT : PolarDensity K T = some ρT) (hU : PolarDensity K (S ∪ T) = some ρ_union) : PolarDensity K S = some (ρ_union - ρT)

theorem RayClassField.polar_density_additive_disjoint {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : (S ∩ T).Finite) (ρS ρT ρU : ℚ) (hρU : ρU = ρS + ρT) : (PolarDensity K S = some ρS → PolarDensity K T = some ρT → PolarDensity K (S ∪ T) = some ρU) ∧ (PolarDensity K S = some ρS → PolarDensity K (S ∪ T) = some ρU → PolarDensity K T = some ρT) ∧ (PolarDensity K T = some ρT → PolarDensity K (S ∪ T) = some ρU → PolarDensity K S = some ρS)

theorem RayClassField.partialDedekindZeta_sdiff_degreeOne_continuousAt {K : Type u_1} [Field K] [NumberField K] (T : Set (Prime' K)) (hT : T ⊆ {𝔭 : Prime' K | ¬IsDegreeOne 𝔭}) : ContinuousAt (partialDedekindZeta K T) 1

theorem RayClassField.partialDedekindZeta_sdiff_degreeOne_analyticAt {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) : AnalyticAt ℂ (partialDedekindZeta K (S \ {𝔭 : Prime' K | IsDegreeOne 𝔭})) 1

theorem RayClassField.summable_norm_eulerFactor_sub_one_of_non_degreeOne {K : Type u_1} [Field K] [NumberField K] (T : Set (Prime' K)) (hT : T ⊆ {𝔭 : Prime' K | ¬IsDegreeOne 𝔭}) : Summable fun (𝔭 : ↑T) => ‖(1 - ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-1))⁻¹ - 1‖

theorem RayClassField.partialDedekindZeta_sdiff_degreeOne_ne_zero {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) : partialDedekindZeta K (S \ {𝔭 : Prime' K | IsDegreeOne 𝔭}) 1 ≠ 0

theorem RayClassField.partialDedekindZeta_sdiff_degreeOne_order {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) : meromorphicOrderAt (partialDedekindZeta K (S \ {𝔭 : Prime' K | IsDegreeOne 𝔭})) 1 = 0

theorem RayClassField.proposition_21_14d_sdiff_degreeOne {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) : PolarDensity K (S \ {𝔭 : Prime' K | IsDegreeOne 𝔭}) = some 0

theorem RayClassField.polar_density_univ {K : Type u_1} [Field K] [NumberField K] : PolarDensity K Set.univ = some 1

theorem RayClassField.proposition_21_14d_degree_one {K : Type u_1} [Field K] [NumberField K] : PolarDensity K {𝔭 : Prime' K | IsDegreeOne 𝔭} = some 1

theorem RayClassField.proposition_21_14d_intersect {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) (hS : PolarDensity K S = some ρ) : PolarDensity K (S ∩ {𝔭 : Prime' K | IsDegreeOne 𝔭}) = some ρ

theorem RayClassField.proposition_21_14d_from_intersect {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) (hS : PolarDensity K (S ∩ {𝔭 : Prime' K | IsDegreeOne 𝔭}) = some ρ) : PolarDensity K S = some ρ

theorem RayClassField.polar_density_nonneg {K : Type u_1} [Field K] [NumberField K] (S : Set (Prime' K)) (ρ : ℚ) (hS : PolarDensity K S = some ρ) : 0 ≤ ρ

def RayClassField.SplitsCompletely (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (𝔭 : Prime' K) : Prop

def RayClassField.Spl (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] : Set (Prime' K)

def RayClassField.SplitsCompletelyGen (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] (𝔭 : Prime' K) : Prop

def RayClassField.SplGen (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] : Set (Prime' K)

theorem RayClassField.spl_degreeOne_crossField_eq (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) (hn : Module.finrank K L = n) (hn_pos : 0 < n) : ∃ (T : Set (Prime' L)), (Set.univ \ T).Finite ∧ partialDedekindZeta K (Spl K L ∩ {𝔭 : Prime' K | IsDegreeOne 𝔭}) ^ n =ᶠ[nhdsWithin 1 {1}ᶜ] partialDedekindZeta L T

theorem RayClassField.spl_degreeOne_nthPower_poleOrder (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) (hn : Module.finrank K L = n) (hn_pos : 0 < n) : HasMeromorphicContinuationWithPoleOrder (partialDedekindZeta K (Spl K L ∩ {𝔭 : Prime' K | IsDegreeOne 𝔭}) ^ n) 1

theorem RayClassField.spl_degree_one_density (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) (hn : Module.finrank K L = n) (hn_pos : 0 < n) : PolarDensity K (Spl K L ∩ {𝔭 : Prime' K | IsDegreeOne 𝔭}) = some (1 / ↑n)

theorem RayClassField.theorem_21_15 (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [IsGalois K L] (n : ℕ) (hn : Module.finrank K L = n) (hn_pos : 0 < n) : PolarDensity K (Spl K L) = some (1 / ↑n)

theorem RayClassField.frobeniusAutomorphism_mem_fixingSubgroup_fieldRange (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] [FiniteDimensional K L] (𝔭 : Prime' K) (h : SplitsCompletelyGen K L 𝔭) (σ : L →ₐ[K] M) : FrobeniusAutomorphism K M 𝔭 ∈ σ.fieldRange.fixingSubgroup

theorem RayClassField.splitsCompletelyGen_of_galois_closure (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] [FiniteDimensional K L] (h_closure : ⨆ (σ : L →ₐ[K] M), σ.fieldRange = ⊤) (𝔭 : Prime' K) (h : SplitsCompletelyGen K L 𝔭) : SplitsCompletely K M 𝔭

theorem RayClassField.arithFrobAt_eq_one_imp_ef_eq_one (K M : Type u) [Field K] [Field M] [NumberField K] [NumberField M] [Algebra K M] [IsGalois K M] (𝔭 : Prime' K) (h : arithFrobAt (NumberField.RingOfIntegers K) Gal(M/K) (choosePrimeOver K M 𝔭) = 1) : 𝔭.asIdeal.ramificationIdxIn (NumberField.RingOfIntegers M) = 1 ∧ 𝔭.asIdeal.inertiaDegIn (NumberField.RingOfIntegers M) = 1

theorem RayClassField.splitsCompletely_imp_splitsCompletelyGen (K M : Type u) [Field K] [Field M] [NumberField K] [NumberField M] [Algebra K M] [IsGalois K M] (𝔭 : Prime' K) (h : SplitsCompletely K M 𝔭) : SplitsCompletelyGen K M 𝔭

theorem RayClassField.splitsCompletelyGen_of_tower (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] (𝔭 : Prime' K) (h : SplitsCompletely K M 𝔭) : SplitsCompletelyGen K L 𝔭

theorem RayClassField.splGen_eq_spl_of_galois_closure (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] [FiniteDimensional K L] (h_closure : ⨆ (σ : L →ₐ[K] M), σ.fieldRange = ⊤) : SplGen K L = Spl K M

theorem RayClassField.corollary_21_16 (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K M] [FiniteDimensional K L] (h_closure : ⨆ (σ : L →ₐ[K] M), σ.fieldRange = ⊤) (n : ℕ) (hn : Module.finrank K M = n) (hn_pos : 0 < n) : SplGen K L = Spl K M ∧ PolarDensity K (SplGen K L) = some (1 / ↑n) ∧ PolarDensity K (Spl K M) = some (1 / ↑n)

theorem RayClassField.corollary_21_17 (K L F : Type u) [Field K] [Field L] [Field F] [NumberField K] [NumberField L] [NumberField F] [Algebra K L] [Algebra K F] [Algebra F L] [IsGalois K L] [IsGalois K F] [IsScalarTower K F L] [FiniteDimensional K L] (H : Subgroup Gal(L/K)) [H.Normal] (hF : (AlgEquiv.restrictNormalHom F).ker = H) : PolarDensity K (Spl K F) = some (↑(Nat.card ↥H) / ↑(Nat.card Gal(L/K)))

def RayClassField.FinSymmDiff {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) : Prop

def RayClassField.PrimeSetLe {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) : Prop

theorem RayClassField.splitsCompletely_of_algHom (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (𝔭 : Prime' K) (f : L →ₐ[K] M) (h : SplitsCompletely K M 𝔭) : SplitsCompletely K L 𝔭

theorem RayClassField.polarDensity_eq_of_finSymmDiff {K : Type u_1} [Field K] [NumberField K] (S T : Set (Prime' K)) (h : FinSymmDiff S T) (ρ : ℚ) (hS : PolarDensity K S = some ρ) : PolarDensity K T = some ρ

theorem RayClassField.adjoin_range_eq_fieldRange {K' : Type u_2} {L' : Type u_3} {E' : Type u_4} [Field K'] [Field L'] [Field E'] [Algebra K' L'] [Algebra K' E'] (f : L' →ₐ[K'] E') : IntermediateField.adjoin K' (Set.range ⇑f) = f.fieldRange

theorem RayClassField.inclusion_fieldRange_sup_eq_top {K' : Type u_2} {A' : Type u_3} [Field K'] [Field A'] [Algebra K' A'] {E' F' : IntermediateField K' A'} : (IntermediateField.inclusion ⋯).fieldRange ⊔ (IntermediateField.inclusion ⋯).fieldRange = ⊤

theorem RayClassField.comp_equiv_fieldRange {K' : Type u_2} {L' : Type u_3} {E' : Type u_4} {F' : Type u_5} [Field K'] [Field L'] [Field E'] [Field F'] [Algebra K' L'] [Algebra K' E'] [Algebra K' F'] (f : E' →ₐ[K'] F') (g : L' ≃ₐ[K'] E') : (f.comp ↑g).fieldRange = f.fieldRange

theorem RayClassField.isUnramifiedAt_comap_of_galois (K' L' M' : Type u) [Field K'] [Field L'] [Field M'] [NumberField K'] [NumberField L'] [NumberField M'] [Algebra K' L'] [Algebra K' M'] [Algebra L' M'] [IsGalois K' L'] [IsGalois K' M'] [IsScalarTower K' L' M'] (𝔭 : Prime' K') (h_sc : SplitsCompletely K' L' 𝔭 := by assumption) : Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K') (Ideal.comap (algebraMap (NumberField.RingOfIntegers L') (NumberField.RingOfIntegers M')) (choosePrimeOver K' M' 𝔭))

theorem RayClassField.compositum_spl_inter_and_degree (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : ∃ (N : Type u) (x : Field N) (x_1 : NumberField N) (x_2 : Algebra K N) (x_3 : IsGalois K N) (x_4 : Algebra M N) (_ : IsScalarTower K M N), Spl K N = Spl K L ∩ Spl K M ∧ (Module.finrank K N = Module.finrank K M → Nonempty (L →ₐ[K] M))

theorem RayClassField.primeSetLe_spl_implies_algHom (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (h : PrimeSetLe (Spl K M) (Spl K L)) : Nonempty (L →ₐ[K] M)

theorem RayClassField.theorem_21_18_forward (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (f : L →ₐ[K] M) : Spl K M ⊆ Spl K L

theorem RayClassField.theorem_21_18_spl_determines (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (h : FinSymmDiff (Spl K L) (Spl K M)) : Nonempty (L ≃ₐ[K] M)

theorem RayClassField.theorem_21_18_algEquiv_spl_eq (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (e : L ≃ₐ[K] M) : Spl K M = Spl K L

theorem RayClassField.primeSetLe_spl_implies_subset (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (h : PrimeSetLe (Spl K M) (Spl K L)) : Spl K M ⊆ Spl K L

theorem RayClassField.finSymmDiff_spl_implies_eq (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (h : FinSymmDiff (Spl K L) (Spl K M)) : Spl K L = Spl K M

theorem RayClassField.theorem_21_18_iff_subset (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : Nonempty (L →ₐ[K] M) ↔ Spl K M ⊆ Spl K L

theorem RayClassField.theorem_21_18_iff_primeSetLe (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : Nonempty (L →ₐ[K] M) ↔ PrimeSetLe (Spl K M) (Spl K L)

theorem RayClassField.theorem_21_18_primeSetLe_iff_subset (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : PrimeSetLe (Spl K M) (Spl K L) ↔ Spl K M ⊆ Spl K L

theorem RayClassField.theorem_21_18_iff_eq (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : Nonempty (L ≃ₐ[K] M) ↔ Spl K M = Spl K L

theorem RayClassField.theorem_21_18_iff_finSymmDiff (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : Nonempty (L ≃ₐ[K] M) ↔ FinSymmDiff (Spl K L) (Spl K M)

theorem RayClassField.theorem_21_18_finSymmDiff_iff_eq (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : FinSymmDiff (Spl K L) (Spl K M) ↔ Spl K L = Spl K M

theorem RayClassField.theorem_21_18_injective (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] (h : Spl K L = Spl K M) : Nonempty (L ≃ₐ[K] M)

theorem RayClassField.splitting_primes_determine_abelian_extensions (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [IsGalois K L] [IsGalois K M] : (Nonempty (L →ₐ[K] M) ↔ Spl K M ⊆ Spl K L) ∧ (Nonempty (L ≃ₐ[K] M) ↔ Spl K M = Spl K L) ∧ (Spl K L = Spl K M → Nonempty (L ≃ₐ[K] M))

theorem RayClassField.split_iff_in_kernel (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) (𝔭 : Prime' K) (h_coprime : 𝔪.toFun (Place.finite 𝔭) = 0) : SplitsCompletely K L 𝔭 ↔ (ArtinMap K L 𝔪) (primeCoprime K 𝔪 𝔭 h_coprime) = 1

theorem RayClassField.modulus_support_finite (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) : {𝔭 : Prime' K | 𝔪.toFun (Place.finite 𝔭) ≠ 0}.Finite

theorem RayClassField.artin_image_fixed_field (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (𝔪 : Modulus K) (h_not_surj : ¬Function.Surjective ⇑(ArtinMap K L 𝔪)) : ∃ (F : Type u) (x : Field F) (x_1 : NumberField F) (x_2 : Algebra K F) (x_3 : IsGalois K F), 1 < Module.finrank K F ∧ (Set.univ \ Spl K F).Finite

theorem RayClassField.theorem_21_19_surjective (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] (habel : ∀ (σ τ : Gal(L/K)), σ * τ = τ * σ) (𝔪 : Modulus K) (hdiv : ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), 𝔪.toFun (Place.finite 𝔭) = 0 → ∀ (𝔔 : Ideal (NumberField.RingOfIntegers L)) [inst : 𝔔.IsPrime], 𝔔.LiesOver 𝔭.asIdeal → Algebra.IsUnramifiedAt (NumberField.RingOfIntegers K) 𝔔) : Function.Surjective ⇑(ArtinMap K L 𝔪)

theorem RayClassField.theorem_21_20_unique (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [KroneckerWeber.IsAbelianExtension K L] [KroneckerWeber.IsAbelianExtension K M] (𝔪 : Modulus K) (hker : (ArtinMap K L 𝔪).ker = (ArtinMap K M 𝔪).ker) : Nonempty (L ≃ₐ[K] M)

theorem RayClassField.rayClassField_unique (K L M : Type u) [Field K] [Field L] [Field M] [NumberField K] [NumberField L] [NumberField M] [Algebra K L] [Algebra K M] [KroneckerWeber.IsAbelianExtension K L] [KroneckerWeber.IsAbelianExtension K M] (𝔪 : Modulus K) (hL : IsRayClassField K L 𝔪) (hM : IsRayClassField K M 𝔪) : Nonempty (L ≃ₐ[K] M)

structure RayClassField.CongruenceSubgroupPair (K : Type u) [Field K] [NumberField K] : Type u

• modulus : Modulus K
• subgroup : Subgroup (FracIdealsCoprime K self.modulus)
• ray_le : RayGroup K self.modulus ≤ self.subgroup

noncomputable def RayClassField.CongruenceSubgroupPair.toAmbientSubgroup {K : Type u} [Field K] [NumberField K] (p : CongruenceSubgroupPair K) : Subgroup (FracIdeal K)ˣ

def RayClassField.CongruenceSubgroupPair.IsEquiv {K : Type u} [Field K] [NumberField K] (p₁ p₂ : CongruenceSubgroupPair K) : Prop

noncomputable def RayClassField.ArtinConductor (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] : Modulus K

def RayClassField.IsHilbertClassField (K L : Type u) [Field K] [Field L] [NumberField K] [NumberField L] [Algebra K L] [KroneckerWeber.IsAbelianExtension K L] : Prop

@[reducible, inline]

abbrev RayClassField.polar_density_additive {K : Type u_2} [Field K] [NumberField K] (S T : Set (Prime' K)) (hST : (S ∩ T).Finite) (ρS ρT : ℚ) (hS : PolarDensity K S = some ρS) (hT : PolarDensity K T = some ρT) : PolarDensity K (S ∪ T) = some (ρS + ρT)