@[reducible, inline]

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

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

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

def RayClassField.RayClassChar.evalIdeal {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔞 : FracIdealsCoprime K 𝔪) : ℂˣ

def RayClassField.RayClassChar.evalIdealC {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔞 : FracIdealsCoprime K 𝔪) : ℂ

noncomputable def RayClassField.RayClassChar.evalPrime {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔭 : Prime' K) : ℂ

theorem RayClassField.RayClassChar.norm_evalIdealC_le_one {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔞 : FracIdealsCoprime K 𝔪) : ‖χ.evalIdealC 𝔞‖ ≤ 1

def RayClassField.RayClassChar.IsPrincipal {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) : Prop

noncomputable def RayClassField.weberEulerFactor {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔭 : Prime' K) (s : ℂ) : ℂ

noncomputable def RayClassField.WeberLFunction (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) : ℂ

theorem RayClassField.RayClassChar.norm_evalPrime_le_one {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔭 : Prime' K) : ‖χ.evalPrime 𝔭‖ ≤ 1

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

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

theorem RayClassField.card_primes_le_card_ideals (K : Type u) [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) [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) [Field K] [NumberField K] (σ : ℝ) (hσ : 1 < σ) : Summable fun (𝔭 : Prime' K) => ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-σ)

noncomputable def RayClassField.toFracIdealsCoprime {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (𝔞 : Ideal (NumberField.RingOfIntegers K)) (h : IsCoprime 𝔞 𝔪.finitePartIdeal) : FracIdealsCoprime K 𝔪

noncomputable def RayClassField.RayClassChar.evalIdealExt {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔞 : Ideal (NumberField.RingOfIntegers K)) : ℂ

theorem RayClassField.RayClassChar.evalIdealExt_eq_zero_of_not_coprime {K : Type u} [Field K] [NumberField K] {𝔪 : Modulus K} (χ : RayClassChar K 𝔪) (𝔞 : Ideal (NumberField.RingOfIntegers K)) (h : ¬IsCoprime 𝔞 𝔪.finitePartIdeal) : χ.evalIdealExt 𝔞 = 0

theorem RayClassField.WeberLFunction_eulerProduct_hasSum (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : HasSum (fun (𝔞 : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ }) => χ.evalIdealExt ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)) (∏' (𝔭 : Prime' K), weberEulerFactor χ 𝔭 s)

theorem RayClassField.WeberLFunction_eq_dirichletSeries (K : Type u) [Field K] [NumberField K] (𝔪 : Modulus K) (χ : RayClassChar K 𝔪) (s : ℂ) (hs : 1 < s.re) : WeberLFunction K 𝔪 χ s = ∑' (𝔞 : { I : Ideal (NumberField.RingOfIntegers K) // I ≠ ⊥ }), χ.evalIdealExt ↑𝔞 * ↑(Ideal.absNorm ↑𝔞) ^ (-s)